Lemmas about List.Subset, List.Sublist, List.IsPrefix, List.IsSuffix, and List.IsInfix.

isPrefixOf

@[simp]

theorem List.isPrefixOf_cons₂_self {α : Type u_1} [BEq α] {as : List α} {bs : List α} [LawfulBEq α] {a : α} : (a :: as).isPrefixOf (a :: bs) = as.isPrefixOf bs

@[simp]

theorem List.isPrefixOf_length_pos_nil {α : Type u_1} [BEq α] {L : List α} (h : 0 < L.length) : L.isPrefixOf [] = false

@[simp]

theorem List.isPrefixOf_replicate {α : Type u_1} [BEq α] {l : List α} {n : Nat} {a : α} : l.isPrefixOf (List.replicate n a) = (decide (l.length ≤ n) && l.all fun (x : α) => x == a)

isSuffixOf

@[simp]

theorem List.isSuffixOf_cons_nil {α : Type u_1} [BEq α] {a : α} {as : List α} : (a :: as).isSuffixOf [] = false

@[simp]

theorem List.isSuffixOf_replicate {α : Type u_1} [BEq α] {l : List α} {n : Nat} {a : α} : l.isSuffixOf (List.replicate n a) = (decide (l.length ≤ n) && l.all fun (x : α) => x == a)

Subset

List subset

theorem List.subset_def {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂

@[simp]

theorem List.nil_subset {α : Type u_1} (l : List α) : [] ⊆ l

@[simp]

theorem List.Subset.refl {α : Type u_1} (l : List α) : l ⊆ l

theorem List.Subset.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃

instance List.instTransSubsetMem {α : Type u_1} : Trans (fun (l₁ l₂ : List α) => l₂ ⊆ l₁) Membership.mem Membership.mem

Equations

• List.instTransSubsetMem = { trans := ⋯ }

instance List.instTransSubset {α : Type u_1} : Trans Subset Subset Subset

Equations

• List.instTransSubset = { trans := ⋯ }

theorem List.subset_cons_self {α : Type u_1} (a : α) (l : List α) : l ⊆ a :: l

theorem List.subset_of_cons_subset {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂

@[simp]

theorem List.subset_cons_of_subset {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} : l₁ ⊆ l₂ → l₁ ⊆ a :: l₂

theorem List.cons_subset_cons {α : Type u_1} {l₁ : List α} {l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a :: l₁ ⊆ a :: l₂

@[simp]

theorem List.cons_subset : ∀ {α : Type u_1} {a : α} {l m : List α}, a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m

@[simp]

theorem List.subset_nil {α : Type u_1} {l : List α} : l ⊆ [] ↔ l = []

theorem List.eq_nil_of_subset_nil {α : Type u_1} {l : List α} : l ⊆ [] → l = []

theorem List.map_subset {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : List.map f l₁ ⊆ List.map f l₂

theorem List.filter_subset {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : List.filter p l₁ ⊆ List.filter p l₂

theorem List.filterMap_subset {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) : List.filterMap f l₁ ⊆ List.filterMap f l₂

theorem List.subset_append_left {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₁ ⊆ l₁ ++ l₂

theorem List.subset_append_right {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₂ ⊆ l₁ ++ l₂

@[simp]

theorem List.subset_append_of_subset_left {α : Type u_1} {l : List α} {l₁ : List α} (l₂ : List α) : l ⊆ l₁ → l ⊆ l₁ ++ l₂

@[simp]

theorem List.subset_append_of_subset_right {α : Type u_1} {l : List α} {l₂ : List α} (l₁ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂

@[simp]

theorem List.append_subset {α : Type u_1} {l₁ : List α} {l₂ : List α} {l : List α} : l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l

theorem List.replicate_subset {α : Type u_1} {n : Nat} {a : α} {l : List α} : List.replicate n a ⊆ l ↔ n = 0 ∨ a ∈ l

theorem List.subset_replicate {α : Type u_1} {n : Nat} {a : α} {l : List α} (h : n ≠ 0) : l ⊆ List.replicate n a ↔ ∀ (x : α), x ∈ l → x = a

@[simp]

theorem List.reverse_subset {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁.reverse ⊆ l₂ ↔ l₁ ⊆ l₂

@[simp]

theorem List.subset_reverse {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ ⊆ l₂.reverse ↔ l₁ ⊆ l₂

Sublist and isSublist

@[simp]

theorem List.nil_sublist {α : Type u_1} (l : List α) : [].Sublist l

@[simp]

theorem List.Sublist.refl {α : Type u_1} (l : List α) : l.Sublist l

theorem List.Sublist.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁.Sublist l₂) (h₂ : l₂.Sublist l₃) : l₁.Sublist l₃

instance List.instTransSublist {α : Type u_1} : Trans List.Sublist List.Sublist List.Sublist

Equations

• List.instTransSublist = { trans := ⋯ }

theorem List.sublist_cons_self {α : Type u_1} (a : α) (l : List α) : l.Sublist (a :: l)

theorem List.sublist_of_cons_sublist : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist l₂ → l₁.Sublist l₂

@[simp]

theorem List.cons_sublist_cons : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist (a :: l₂) ↔ l₁.Sublist l₂

theorem List.sublist_or_mem_of_sublist : ∀ {α : Type u_1} {l l₁ : List α} {a : α} {l₂ : List α}, l.Sublist (l₁ ++ a :: l₂) → l.Sublist (l₁ ++ l₂) ∨ a ∈ l

theorem List.Sublist.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁ ⊆ l₂

theorem List.Sublist.mem : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, a ∈ l₁ → l₁.Sublist l₂ → a ∈ l₂

theorem List.Sublist.head_mem : ∀ {α : Type u_1} {ys xs : List α}, ys.Sublist xs → ∀ (h : ys ≠ []), ys.head h ∈ xs

theorem List.Sublist.getLast_mem : ∀ {α : Type u_1} {ys xs : List α}, ys.Sublist xs → ∀ (h : ys ≠ []), ys.getLast h ∈ xs

instance List.instTransSublistSubset {α : Type u_1} : Trans List.Sublist Subset Subset

Equations

• List.instTransSublistSubset = { trans := ⋯ }

instance List.instTransSubsetSublist {α : Type u_1} : Trans Subset List.Sublist Subset

Equations

• List.instTransSubsetSublist = { trans := ⋯ }

instance List.instTransSublistMem {α : Type u_1} : Trans (fun (l₁ l₂ : List α) => l₂.Sublist l₁) Membership.mem Membership.mem

Equations

• List.instTransSublistMem = { trans := ⋯ }

theorem List.mem_of_cons_sublist {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} (s : (a :: l₁).Sublist l₂) : a ∈ l₂

@[simp]

theorem List.sublist_nil {α : Type u_1} {l : List α} : l.Sublist [] ↔ l = []

theorem List.eq_nil_of_sublist_nil {α : Type u_1} {l : List α} (s : l.Sublist []) : l = []

theorem List.Sublist.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length ≤ l₂.length

theorem List.Sublist.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length = l₂.length → l₁ = l₂

theorem List.Sublist.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₂.length ≤ l₁.length → l₁ = l₂

theorem List.Sublist.length_eq : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → (l₁.length = l₂.length ↔ l₁ = l₂)

theorem List.tail_sublist {α : Type u_1} (l : List α) : l.tail.Sublist l

theorem List.Sublist.tail {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁.Sublist l₂ → l₁.tail.Sublist l₂.tail

theorem List.Sublist.of_cons_cons {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} {b : α} (h : (a :: l₁).Sublist (b :: l₂)) : l₁.Sublist l₂

theorem List.Sublist.map {α : Type u_1} {β : Type u_2} (f : α → β) {l₁ : List α} {l₂ : List α} (s : l₁.Sublist l₂) : (List.map f l₁).Sublist (List.map f l₂)

theorem List.Sublist.filterMap {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : α → Option β) (s : l₁.Sublist l₂) : (List.filterMap f l₁).Sublist (List.filterMap f l₂)

theorem List.Sublist.filter {α : Type u_1} (p : α → Bool) {l₁ : List α} {l₂ : List α} (s : l₁.Sublist l₂) : (List.filter p l₁).Sublist (List.filter p l₂)

theorem List.head_filter_mem {α : Type u_1} (xs : List α) (p : α → Bool) (h : List.filter p xs ≠ []) : (List.filter p xs).head h ∈ xs

theorem List.getLast_filter_mem {α : Type u_1} (xs : List α) (p : α → Bool) (h : List.filter p xs ≠ []) : (List.filter p xs).getLast h ∈ xs

theorem List.sublist_filterMap_iff {β : Type u_1} {α : Type u_2} {l₂ : List α} {l₁ : List β} {f : α → Option β} : l₁.Sublist (List.filterMap f l₂) ↔ ∃ (l' : List α), l'.Sublist l₂ ∧ l₁ = List.filterMap f l'

theorem List.sublist_map_iff {β : Type u_1} {α : Type u_2} {l₂ : List α} {l₁ : List β} {f : α → β} : l₁.Sublist (List.map f l₂) ↔ ∃ (l' : List α), l'.Sublist l₂ ∧ l₁ = List.map f l'

theorem List.sublist_filter_iff {α : Type u_1} {l₂ : List α} {l₁ : List α} {p : α → Bool} : l₁.Sublist (List.filter p l₂) ↔ ∃ (l' : List α), l'.Sublist l₂ ∧ l₁ = List.filter p l'

theorem List.sublist_append_left {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₁.Sublist (l₁ ++ l₂)

theorem List.sublist_append_right {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₂.Sublist (l₁ ++ l₂)

@[simp]

theorem List.singleton_sublist {α : Type u_1} {a : α} {l : List α} : [a].Sublist l ↔ a ∈ l

@[simp]

theorem List.sublist_append_of_sublist_left : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Sublist l₁ → l.Sublist (l₁ ++ l₂)

@[simp]

theorem List.sublist_append_of_sublist_right : ∀ {α : Type u_1} {l l₂ l₁ : List α}, l.Sublist l₂ → l.Sublist (l₁ ++ l₂)

@[simp]

theorem List.append_sublist_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l ++ l₁).Sublist (l ++ l₂) ↔ l₁.Sublist l₂

theorem List.Sublist.append_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∀ (l : List α), (l ++ l₁).Sublist (l ++ l₂)

theorem List.Sublist.append_right : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∀ (l : List α), (l₁ ++ l).Sublist (l₂ ++ l)

theorem List.Sublist.append : ∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α}, l₁.Sublist l₂ → r₁.Sublist r₂ → (l₁ ++ r₁).Sublist (l₂ ++ r₂)

theorem List.sublist_cons_iff {α : Type u_1} {a : α} {l : List α} {l' : List α} : l.Sublist (a :: l') ↔ l.Sublist l' ∨ ∃ (r : List α), l = a :: r ∧ r.Sublist l'

theorem List.cons_sublist_iff {α : Type u_1} {a : α} {l : List α} {l' : List α} : (a :: l).Sublist l' ↔ ∃ (r₁ : List α), ∃ (r₂ : List α), l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l.Sublist r₂

theorem List.sublist_append_iff {α : Type u_1} {r₁ : List α} {r₂ : List α} {l : List α} : l.Sublist (r₁ ++ r₂) ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ l₁.Sublist r₁ ∧ l₂.Sublist r₂

theorem List.append_sublist_iff {α : Type u_1} {r : List α} {l₁ : List α} {l₂ : List α} : (l₁ ++ l₂).Sublist r ↔ ∃ (r₁ : List α), ∃ (r₂ : List α), r = r₁ ++ r₂ ∧ l₁.Sublist r₁ ∧ l₂.Sublist r₂

theorem List.Sublist.of_sublist_append_left : ∀ {α : Type u_1} {l l₂ l₁ : List α}, (∀ (a : α), a ∈ l → ¬a ∈ l₂) → l.Sublist (l₁ ++ l₂) → l.Sublist l₁

theorem List.Sublist.of_sublist_append_right : ∀ {α : Type u_1} {l l₁ l₂ : List α}, (∀ (a : α), a ∈ l → ¬a ∈ l₁) → l.Sublist (l₁ ++ l₂) → l.Sublist l₂

theorem List.Sublist.middle {α : Type u_1} {l₁ : List α} {l₂ : List α} {l : List α} (h : l.Sublist (l₁ ++ l₂)) (a : α) : l.Sublist (l₁ ++ a :: l₂)

theorem List.Sublist.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.reverse.Sublist l₂.reverse

@[simp]

theorem List.reverse_sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse.Sublist l₂.reverse ↔ l₁.Sublist l₂

theorem List.sublist_reverse_iff : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂.reverse ↔ l₁.reverse.Sublist l₂

@[simp]

theorem List.append_sublist_append_right : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l₁ ++ l).Sublist (l₂ ++ l) ↔ l₁.Sublist l₂

@[simp]

theorem List.replicate_sublist_replicate {α : Type u_1} {m : Nat} {n : Nat} (a : α) : (List.replicate m a).Sublist (List.replicate n a) ↔ m ≤ n

theorem List.sublist_replicate_iff : ∀ {α : Type u_1} {l : List α} {m : Nat} {a : α}, l.Sublist (List.replicate m a) ↔ ∃ (n : Nat), n ≤ m ∧ l = List.replicate n a

theorem List.sublist_join_of_mem {α : Type u_1} {L : List (List α)} {l : List α} (h : l ∈ L) : l.Sublist L.join

theorem List.sublist_join_iff {α : Type u_1} {L : List (List α)} {l : List α} : l.Sublist L.join ↔ ∃ (L' : List (List α)), l = L'.join ∧ ∀ (i : Nat) (x : i < L'.length), L'[i].Sublist (L[i]?.getD [])

theorem List.join_sublist_iff {α : Type u_1} {L : List (List α)} {l : List α} : L.join.Sublist l ↔ ∃ (L' : List (List α)), l = L'.join ∧ ∀ (i : Nat) (x : i < L.length), L[i].Sublist (L'[i]?.getD [])

@[simp]

theorem List.isSublist_iff_sublist {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ : List α} {l₂ : List α} : l₁.isSublist l₂ = true ↔ l₁.Sublist l₂

instance List.instDecidableSublistOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) : Decidable (l₁.Sublist l₂)

Equations

• l₁.instDecidableSublistOfDecidableEq l₂ = decidable_of_iff (l₁.isSublist l₂ = true) ⋯

theorem List.Sublist.drop {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁.Sublist l₂ → ∀ (n : Nat), (List.drop n l₁).Sublist (List.drop n l₂)

IsPrefix / IsSuffix / IsInfix

@[simp]

theorem List.prefix_append {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₁ <+: l₁ ++ l₂

@[simp]

theorem List.suffix_append {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₂ <:+ l₁ ++ l₂

theorem List.infix_append {α : Type u_1} (l₁ : List α) (l₂ : List α) (l₃ : List α) : l₂ <:+: l₁ ++ l₂ ++ l₃

@[simp]

theorem List.infix_append' {α : Type u_1} (l₁ : List α) (l₂ : List α) (l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃)

theorem List.IsPrefix.isInfix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁ <:+: l₂

theorem List.IsSuffix.isInfix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁ <:+: l₂

@[simp]

theorem List.nil_prefix {α : Type u_1} {l : List α} : [] <+: l

@[simp]

theorem List.nil_suffix {α : Type u_1} {l : List α} : [] <:+ l

@[simp]

theorem List.nil_infix {α : Type u_1} {l : List α} : [] <:+: l

theorem List.prefix_refl {α : Type u_1} (l : List α) : l <+: l

@[simp]

theorem List.prefix_rfl {α : Type u_1} {l : List α} : l <+: l

theorem List.suffix_refl {α : Type u_1} (l : List α) : l <:+ l

@[simp]

theorem List.suffix_rfl {α : Type u_1} {l : List α} : l <:+ l

theorem List.infix_refl {α : Type u_1} (l : List α) : l <:+: l

@[simp]

theorem List.infix_rfl {α : Type u_1} {l : List α} : l <:+: l

@[simp]

theorem List.suffix_cons {α : Type u_1} (a : α) (l : List α) : l <:+ a :: l

theorem List.infix_cons : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+: l₂ → l₁ <:+: a :: l₂

theorem List.infix_concat : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+: l₂ → l₁ <:+: l₂.concat a

theorem List.IsPrefix.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} : l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃

theorem List.IsSuffix.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} : l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃

theorem List.IsInfix.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} : l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃

theorem List.IsInfix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.Sublist l₂

theorem List.IsInfix.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁ ⊆ l₂

theorem List.IsPrefix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.Sublist l₂

theorem List.IsPrefix.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁ ⊆ l₂

theorem List.IsSuffix.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.Sublist l₂

theorem List.IsSuffix.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁ ⊆ l₂

@[simp]

theorem List.infix_nil : ∀ {α : Type u_1} {l : List α}, l <:+: [] ↔ l = []

@[simp]

theorem List.prefix_nil : ∀ {α : Type u_1} {l : List α}, l <+: [] ↔ l = []

@[simp]

theorem List.suffix_nil : ∀ {α : Type u_1} {l : List α}, l <:+ [] ↔ l = []

theorem List.eq_nil_of_infix_nil : ∀ {α : Type u_1} {l : List α}, l <:+: [] → l = []

theorem List.eq_nil_of_prefix_nil : ∀ {α : Type u_1} {l : List α}, l <+: [] → l = []

theorem List.eq_nil_of_suffix_nil : ∀ {α : Type u_1} {l : List α}, l <:+ [] → l = []

theorem List.IsPrefix.ne_nil {α : Type u_1} {x : List α} {y : List α} (h : x <+: y) (hx : x ≠ []) : y ≠ []

theorem List.IsSuffix.ne_nil {α : Type u_1} {x : List α} {y : List α} (h : x <:+ y) (hx : x ≠ []) : y ≠ []

theorem List.IsInfix.ne_nil {α : Type u_1} {x : List α} {y : List α} (h : x <:+: y) (hx : x ≠ []) : y ≠ []

theorem List.IsInfix.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.length ≤ l₂.length

theorem List.IsPrefix.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.length ≤ l₂.length

theorem List.IsSuffix.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.length ≤ l₂.length

theorem List.IsPrefix.getElem {α : Type u_1} {x : List α} {y : List α} (h : x <+: y) {n : Nat} (hn : n < x.length) : x[n] = y[n]

theorem List.IsPrefix.mem : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, a ∈ l₁ → l₁ <+: l₂ → a ∈ l₂

theorem List.IsSuffix.mem : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, a ∈ l₁ → l₁ <:+ l₂ → a ∈ l₂

theorem List.IsInfix.mem : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, a ∈ l₁ → l₁ <:+: l₂ → a ∈ l₂

@[simp]

theorem List.reverse_suffix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <:+ l₂.reverse ↔ l₁ <+: l₂

@[simp]

theorem List.reverse_prefix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <+: l₂.reverse ↔ l₁ <:+ l₂

@[simp]

theorem List.reverse_infix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <:+: l₂.reverse ↔ l₁ <:+: l₂

theorem List.IsInfix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.reverse <:+: l₂.reverse

theorem List.IsSuffix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.reverse <+: l₂.reverse

theorem List.IsPrefix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.reverse <:+ l₂.reverse

theorem List.IsPrefix.head {α : Type u_1} {x : List α} {y : List α} (h : x <+: y) (hx : x ≠ []) : x.head hx = y.head ⋯

theorem List.IsSuffix.getLast {α : Type u_1} {x : List α} {y : List α} (h : x <:+ y) (hx : x ≠ []) : x.getLast hx = y.getLast ⋯

theorem List.prefix_concat {α : Type u_1} (a : α) (l : List α) : l <+: l.concat a

theorem List.infix_iff_prefix_suffix {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ <:+: l₂ ↔ ∃ (t : List α), l₁ <+: t ∧ t <:+ l₂

theorem List.infix_iff_suffix_prefix {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ <:+: l₂ ↔ ∃ (t : List α), l₁ <:+ t ∧ t <+: l₂

theorem List.IsInfix.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.length = l₂.length → l₁ = l₂

theorem List.IsInfix.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₂.length ≤ l₁.length → l₁ = l₂

theorem List.IsPrefix.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.length = l₂.length → l₁ = l₂

theorem List.IsPrefix.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₂.length ≤ l₁.length → l₁ = l₂

theorem List.IsSuffix.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.length = l₂.length → l₁ = l₂

theorem List.IsSuffix.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₂.length ≤ l₁.length → l₁ = l₂

theorem List.prefix_of_prefix_length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} : l₁ <+: l₃ → l₂ <+: l₃ → l₁.length ≤ l₂.length → l₁ <+: l₂

theorem List.prefix_or_prefix_of_prefix : ∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → l₁ <+: l₂ ∨ l₂ <+: l₁

theorem List.suffix_of_suffix_length_le : ∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+ l₃ → l₂ <:+ l₃ → l₁.length ≤ l₂.length → l₁ <:+ l₂

theorem List.suffix_or_suffix_of_suffix : ∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+ l₃ → l₂ <:+ l₃ → l₁ <:+ l₂ ∨ l₂ <:+ l₁

theorem List.prefix_cons_iff : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <+: a :: l₂ ↔ l₁ = [] ∨ ∃ (t : List α), l₁ = a :: t ∧ t <+: l₂

@[simp]

theorem List.cons_prefix_cons : ∀ {α : Type u_1} {a : α} {l₁ : List α} {b : α} {l₂ : List α}, a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂

theorem List.suffix_cons_iff : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂

theorem List.infix_cons_iff : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂

theorem List.prefix_concat_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} : l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂

theorem List.suffix_concat_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} : l₁ <:+ l₂ ++ [a] ↔ l₁ = [] ∨ ∃ (t : List α), l₁ = t ++ [a] ∧ t <:+ l₂

theorem List.infix_concat_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} : l₁ <:+: l₂ ++ [a] ↔ l₁ <:+ l₂ ++ [a] ∨ l₁ <:+: l₂

theorem List.isPrefix_iff : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ ↔ ∀ (i : Nat) (h : i < l₁.length), l₂[i]? = some l₁[i]

theorem List.isPrefix_iff_getElem {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ (x : Nat) (hx : x < l₁.length), l₁[x] = l₂[x]

theorem List.isPrefix_filterMap_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <+: List.filterMap f l₁ ↔ ∃ (l : List α), l <+: l₁ ∧ l₂ = List.filterMap f l

theorem List.isSuffix_filterMap_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <:+ List.filterMap f l₁ ↔ ∃ (l : List α), l <:+ l₁ ∧ l₂ = List.filterMap f l

theorem List.isInfix_filterMap_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l₁ : List α} {l₂ : List β} : l₂ <:+: List.filterMap f l₁ ↔ ∃ (l : List α), l <:+: l₁ ∧ l₂ = List.filterMap f l

theorem List.isPrefix_filter_iff {α : Type u_1} {p : α → Bool} {l₁ : List α} {l₂ : List α} : l₂ <+: List.filter p l₁ ↔ ∃ (l : List α), l <+: l₁ ∧ l₂ = List.filter p l

theorem List.isSuffix_filter_iff {α : Type u_1} {p : α → Bool} {l₁ : List α} {l₂ : List α} : l₂ <:+ List.filter p l₁ ↔ ∃ (l : List α), l <:+ l₁ ∧ l₂ = List.filter p l

theorem List.isInfix_filter_iff {α : Type u_1} {p : α → Bool} {l₁ : List α} {l₂ : List α} : l₂ <:+: List.filter p l₁ ↔ ∃ (l : List α), l <:+: l₁ ∧ l₂ = List.filter p l

theorem List.isPrefix_map_iff {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <+: List.map f l₁ ↔ ∃ (l : List α), l <+: l₁ ∧ l₂ = List.map f l

theorem List.isSuffix_map_iff {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <:+ List.map f l₁ ↔ ∃ (l : List α), l <:+ l₁ ∧ l₂ = List.map f l

theorem List.isInfix_map_iff {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : List α} {l₂ : List β} : l₂ <:+: List.map f l₁ ↔ ∃ (l : List α), l <:+: l₁ ∧ l₂ = List.map f l

theorem List.isPrefix_replicate_iff {α : Type u_1} {n : Nat} {a : α} {l : List α} : l <+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a

theorem List.isSuffix_replicate_iff {α : Type u_1} {n : Nat} {a : α} {l : List α} : l <:+ List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a

theorem List.isInfix_replicate_iff {α : Type u_1} {n : Nat} {a : α} {l : List α} : l <:+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a

theorem List.infix_of_mem_join {α : Type u_1} {l : List α} {L : List (List α)} : l ∈ L → l <:+: L.join

theorem List.prefix_append_right_inj : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂

theorem List.prefix_cons_inj : ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂

theorem List.take_prefix {α : Type u_1} (n : Nat) (l : List α) : List.take n l <+: l

theorem List.drop_suffix {α : Type u_1} (n : Nat) (l : List α) : List.drop n l <:+ l

theorem List.take_sublist {α : Type u_1} (n : Nat) (l : List α) : (List.take n l).Sublist l

theorem List.drop_sublist {α : Type u_1} (n : Nat) (l : List α) : (List.drop n l).Sublist l

theorem List.take_subset {α : Type u_1} (n : Nat) (l : List α) : List.take n l ⊆ l

theorem List.drop_subset {α : Type u_1} (n : Nat) (l : List α) : List.drop n l ⊆ l

theorem List.mem_of_mem_take {α : Type u_1} {n : Nat} {a : α} {l : List α} (h : a ∈ List.take n l) : a ∈ l

theorem List.mem_of_mem_drop {α : Type u_1} {a : α} {n : Nat} {l : List α} (h : a ∈ List.drop n l) : a ∈ l

theorem List.drop_suffix_drop_left {α : Type u_1} (l : List α) {m : Nat} {n : Nat} (h : m ≤ n) : List.drop n l <:+ List.drop m l

theorem List.drop_sublist_drop_left {α : Type u_1} (l : List α) {m : Nat} {n : Nat} (h : m ≤ n) : (List.drop n l).Sublist (List.drop m l)

theorem List.drop_subset_drop_left {α : Type u_1} (l : List α) {m : Nat} {n : Nat} (h : m ≤ n) : List.drop n l ⊆ List.drop m l

theorem List.takeWhile_prefix {α : Type u_1} {l : List α} (p : α → Bool) : List.takeWhile p l <+: l

theorem List.dropWhile_suffix {α : Type u_1} {l : List α} (p : α → Bool) : List.dropWhile p l <:+ l

theorem List.takeWhile_sublist {α : Type u_1} {l : List α} (p : α → Bool) : (List.takeWhile p l).Sublist l

theorem List.dropWhile_sublist {α : Type u_1} {l : List α} (p : α → Bool) : (List.dropWhile p l).Sublist l

theorem List.takeWhile_subset {α : Type u_1} {l : List α} (p : α → Bool) : List.takeWhile p l ⊆ l

theorem List.dropWhile_subset {α : Type u_1} {l : List α} (p : α → Bool) : List.dropWhile p l ⊆ l

theorem List.dropLast_prefix {α : Type u_1} (l : List α) : l.dropLast <+: l

theorem List.dropLast_sublist {α : Type u_1} (l : List α) : l.dropLast.Sublist l

theorem List.dropLast_subset {α : Type u_1} (l : List α) : l.dropLast ⊆ l

theorem List.tail_suffix {α : Type u_1} (l : List α) : l.tail <:+ l

theorem List.IsPrefix.map {α : Type u_1} {β : Type u_2} (f : α → β) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <+: l₂) : List.map f l₁ <+: List.map f l₂

theorem List.IsSuffix.map {α : Type u_1} {β : Type u_2} (f : α → β) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+ l₂) : List.map f l₁ <:+ List.map f l₂

theorem List.IsInfix.map {α : Type u_1} {β : Type u_2} (f : α → β) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+: l₂) : List.map f l₁ <:+: List.map f l₂

theorem List.IsPrefix.filter {α : Type u_1} (p : α → Bool) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <+: l₂) : List.filter p l₁ <+: List.filter p l₂

theorem List.IsSuffix.filter {α : Type u_1} (p : α → Bool) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+ l₂) : List.filter p l₁ <:+ List.filter p l₂

theorem List.IsInfix.filter {α : Type u_1} (p : α → Bool) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+: l₂) : List.filter p l₁ <:+: List.filter p l₂

theorem List.IsPrefix.filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <+: l₂) : List.filterMap f l₁ <+: List.filterMap f l₂

theorem List.IsSuffix.filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+ l₂) : List.filterMap f l₁ <:+ List.filterMap f l₂

theorem List.IsInfix.filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+: l₂) : List.filterMap f l₁ <:+: List.filterMap f l₂

@[simp]

theorem List.isPrefixOf_iff_prefix {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ : List α} {l₂ : List α} : l₁.isPrefixOf l₂ = true ↔ l₁ <+: l₂

instance List.instDecidableIsPrefixOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) : Decidable (l₁ <+: l₂)

Equations

• l₁.instDecidableIsPrefixOfDecidableEq l₂ = decidable_of_iff (l₁.isPrefixOf l₂ = true) ⋯

@[simp]

theorem List.isSuffixOf_iff_suffix {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ : List α} {l₂ : List α} : l₁.isSuffixOf l₂ = true ↔ l₁ <:+ l₂

instance List.instDecidableIsSuffixOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) : Decidable (l₁ <:+ l₂)

Equations

• l₁.instDecidableIsSuffixOfDecidableEq l₂ = decidable_of_iff (l₁.isSuffixOf l₂ = true) ⋯

theorem List.prefix_iff_eq_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ ↔ l₁ ++ List.drop l₁.length l₂ = l₂

theorem List.prefix_iff_eq_take : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ ↔ l₁ = List.take l₁.length l₂