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

isPrefixOf

@[simp]

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

@[deprecated List.isPrefixOf_cons_cons_self (since := "2026-02-26")]

theorem List.isPrefixOf_cons₂_self {α : Type u_1} [BEq α] {as 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 (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 (replicate n a) = (decide (l.length ≤ n) && l.all fun (x : α) => x == a)

Subset

List subset

theorem List.subset_def {α : Type u_1} {l₁ 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₁ l₂ l₃ : List α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃

@[instance_reducible]

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

Equations

• List.instTransSubsetMem = { trans := ⋯ }

@[instance_reducible]

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₁ l₂ : List α} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂

@[simp]

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

theorem List.cons_subset_cons {α : Type u_1} {l₁ 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₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem List.replicate_subset {α : Type u_1} {n : Nat} {a : α} {l : 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 ⊆ replicate n a ↔ ∀ (x : α), x ∈ l → x = a

@[simp]

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

@[simp]

theorem List.subset_reverse {α : Type u_1} {l₁ 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₁ l₂ l₃ : List α} (h₁ : l₁.Sublist l₂) (h₂ : l₂.Sublist l₃) : l₁.Sublist l₃

@[instance_reducible]

instance List.instTransSublist {α : Type u_1} : Trans Sublist Sublist 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 α✝} (h : 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 α✝} (hx : a ∈ l₁) (hl : l₁.Sublist l₂) : a ∈ l₂

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

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

@[instance_reducible]

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

Equations

• List.instTransSublistSubset = { trans := ⋯ }

@[instance_reducible]

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

Equations

• List.instTransSubsetSublist = { trans := ⋯ }

@[instance_reducible]

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₁ 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 α✝} (s : l₁.Sublist l₂) (h : l₂.length ≤ l₁.length) : l₁ = l₂

theorem List.Sublist.length_eq {α✝ : Type u_1} {l₁ l₂ : List α✝} (s : 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₁ l₂ : List α} : l₁.Sublist l₂ → l₁.tail.Sublist l₂.tail

theorem List.Sublist.of_cons_cons {α : Type u_1} {l₁ 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₁ l₂ : List α} (s : l₁.Sublist l₂) : (map f l₁).Sublist (map f l₂)

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

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

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

theorem List.getLast_filter_mem {α : Type u_1} (xs : List α) (p : α → Bool) (h : filter p xs ≠ []) : (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 (filterMap f l₂) ↔ ∃ (l' : List α), l'.Sublist l₂ ∧ l₁ = filterMap f l'

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

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

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

theorem List.sublist_append_right {α : Type u_1} (l₁ 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 α✝} (s : l.Sublist l₁) : l.Sublist (l₁ ++ l₂)

@[simp]

theorem List.sublist_append_of_sublist_right {α✝ : Type u_1} {l l₂ l₁ : List α✝} (s : 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 α✝} (hl : l₁.Sublist l₂) (hr : r₁.Sublist r₂) : (l₁ ++ r₁).Sublist (l₂ ++ r₂)

theorem List.sublist_cons_iff {α : Type u_1} {a : α} {l 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 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₁ r₂ 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 l₁ 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 α✝} (w : ∀ (a : α✝), a ∈ l → ¬a ∈ l₂) (h : l.Sublist (l₁ ++ l₂)) : l.Sublist l₁

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

theorem List.Sublist.middle {α : Type u_1} {l₁ l₂ 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 n : Nat} (a : α) : (replicate m a).Sublist (replicate n a) ↔ m ≤ n

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

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

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

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

@[simp]

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

@[instance_reducible]

instance List.instDecidableSublistOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ 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₁ l₂ : List α} : l₁.Sublist l₂ → ∀ (i : Nat), (drop i l₁).Sublist (drop i l₂)

IsPrefix / IsSuffix / IsInfix

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem List.infix_append_left {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+: l₁ ++ l₂

theorem List.infix_append_right {α✝ : Type u_1} {l₂ l₁ : List α✝} : 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

@[simp]

theorem List.suffix_cons_append {α : Type u_1} {a : α} {l₁ l₂ : List α} : l₂ <:+ a :: (l₁ ++ 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₁ l₂ l₃ : List α} : l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃

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

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

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

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

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

theorem List.infix_append_of_infix_right {α✝ : Type u_1} {l₁ l₃ l₂ : List α✝} (h : 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 α✝} (hl : l₁ <:+: l₂) : l₁ ⊆ l₂

theorem List.IsPrefix.sublist {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <+: l₂) : l₁.Sublist l₂

theorem List.IsPrefix.subset {α✝ : Type u_1} {l₁ l₂ : List α✝} (hl : l₁ <+: l₂) : l₁ ⊆ l₂

theorem List.IsSuffix.sublist {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+ l₂) : l₁.Sublist l₂

theorem List.IsSuffix.subset {α✝ : Type u_1} {l₁ l₂ : List α✝} (hl : 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 α✝} (h : l <:+: []) : l = []

theorem List.eq_nil_of_prefix_nil {α✝ : Type u_1} {l : List α✝} (h : l <+: []) : l = []

theorem List.eq_nil_of_suffix_nil {α✝ : Type u_1} {l : List α✝} (h : l <:+ []) : l = []

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

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

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

theorem List.IsInfix.length_le {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length

theorem List.IsPrefix.length_le {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <+: l₂) : l₁.length ≤ l₂.length

theorem List.IsSuffix.length_le {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length

theorem List.IsPrefix.getElem {α : Type u_1} {xs ys : List α} (h : xs <+: ys) {i : Nat} (hi : i < xs.length) : xs[i] = ys[i]

theorem List.IsPrefix.mem {α✝ : Type u_1} {l₁ : List α✝} {a : α✝} {l₂ : List α✝} (hx : a ∈ l₁) (hl : l₁ <+: l₂) : a ∈ l₂

theorem List.IsSuffix.mem {α✝ : Type u_1} {l₁ : List α✝} {a : α✝} {l₂ : List α✝} (hx : a ∈ l₁) (hl : l₁ <:+ l₂) : a ∈ l₂

theorem List.IsInfix.mem {α✝ : Type u_1} {l₁ : List α✝} {a : α✝} {l₂ : List α✝} (hx : a ∈ l₁) (hl : 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} {l₁ l₂ : List α} (h : l₁ <+: l₂) (hx : l₁ ≠ []) : l₁.head hx = l₂.head ⋯

theorem List.IsSuffix.getLast {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <:+ l₂) (hx : l₁ ≠ []) : l₁.getLast hx = l₂.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₁ l₂ : List α} : l₁ <:+: l₂ ↔ ∃ (t : List α), l₁ <+: t ∧ t <:+ l₂

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

theorem List.IsInfix.eq_of_length {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+: l₂) : l₁.length = l₂.length → l₁ = l₂

theorem List.IsInfix.eq_of_length_le {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+: l₂) : l₂.length ≤ l₁.length → l₁ = l₂

theorem List.IsPrefix.eq_of_length {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <+: l₂) : l₁.length = l₂.length → l₁ = l₂

theorem List.IsPrefix.eq_of_length_le {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <+: l₂) : l₂.length ≤ l₁.length → l₁ = l₂

theorem List.IsSuffix.eq_of_length {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+ l₂) : l₁.length = l₂.length → l₁ = l₂

theorem List.IsSuffix.eq_of_length_le {α✝ : Type u_1} {l₁ l₂ : List α✝} (h : l₁ <:+ l₂) : l₂.length ≤ l₁.length → l₁ = l₂

theorem List.prefix_of_prefix_length_le {α : Type u_1} {l₁ l₂ 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 α✝} (h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) : l₁ <+: l₂ ∨ l₂ <+: l₁

theorem List.suffix_of_suffix_length_le {α✝ : Type u_1} {l₁ l₃ l₂ : List α✝} (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : l₁.length ≤ l₂.length) : l₁ <:+ l₂

theorem List.suffix_or_suffix_of_suffix {α✝ : Type u_1} {l₁ l₃ l₂ : List α✝} (h₁ : l₁ <:+ l₃) (h₂ : 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₁ l₂ : List α} {a : α} : l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂

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

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

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

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

theorem List.cons_prefix_iff {α : Type u_1} {a : α} {l₁ l₂ : List α} : a :: l₁ <+: l₂ ↔ ∃ (l' : List α), l₂ = a :: l' ∧ l₁ <+: l'

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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} (i : Nat) (l : List α) : take i l <+: l

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem List.dropWhile_subset {α : Type u_1} {l : List α} (p : α → Bool) : 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₁ 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₁ 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₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : List.map f l₁ <:+: List.map f l₂

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

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

theorem List.IsInfix.filter {α : Type u_1} (p : α → Bool) ⦃l₁ 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₁ 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₁ 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₁ 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₁ l₂ : List α} : l₁.isPrefixOf l₂ = true ↔ l₁ <+: l₂

@[instance_reducible]

instance List.instDecidableIsPrefixOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ 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₁ l₂ : List α} : l₁.isSuffixOf l₂ = true ↔ l₁ <:+ l₂

@[instance_reducible]

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

Equations

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

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

@[instance_reducible]

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

Equations

• l₁.instDecidableIsInfixOfDecidableEq l₂ = decidable_of_iff (l₁.isInfixOf_internal l₂ = true) ⋯

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

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

theorem List.prefix_iff_exists_append_eq {α : Type u_1} {l₁ l₂ : List α} : l₁ <+: l₂ ↔ ∃ (l₃ : List α), l₁ ++ l₃ = l₂

theorem List.prefix_iff_exists_eq_append {α : Type u_1} {l₁ l₂ : List α} : l₁ <+: l₂ ↔ ∃ (l₃ : List α), l₂ = l₁ ++ l₃

theorem List.suffix_iff_exists_append_eq {α : Type u_1} {l₁ l₂ : List α} : l₁ <:+ l₂ ↔ ∃ (l₃ : List α), l₃ ++ l₁ = l₂

theorem List.suffix_iff_exists_eq_append {α : Type u_1} {l₁ l₂ : List α} : l₁ <:+ l₂ ↔ ∃ (l₃ : List α), l₂ = l₃ ++ l₁

theorem List.suffix_append_self_iff {α : Type u_1} {l₁ l₂ l₃ : List α} : l₁ ++ l₃ <:+ l₂ ++ l₃ ↔ l₁ <:+ l₂

theorem List.prefix_self_append_iff {α : Type u_1} {l₁ l₂ l₃ : List α} : l₃ ++ l₁ <+: l₃ ++ l₂ ↔ l₁ <+: l₂

theorem List.suffix_append_inj_of_length_eq {α : Type u_1} {l₁ l₂ s₁ s₂ : List α} (hs : s₁.length = s₂.length) : l₁ ++ s₁ <:+ l₂ ++ s₂ ↔ l₁ <:+ l₂ ∧ s₁ = s₂

theorem List.prefix_append_inj_of_length_eq {α : Type u_1} {l₁ l₂ s₁ s₂ : List α} (hs : s₁.length = s₂.length) : s₁ ++ l₁ <+: s₂ ++ l₂ ↔ s₁ = s₂ ∧ l₁ <+: l₂

theorem List.singleton_suffix_iff_getLast?_eq_some {α : Type u_1} {a : α} {l : List α} : [a] <:+ l ↔ l.getLast? = some a

theorem List.singleton_prefix_iff_head?_eq_some {α : Type u_1} {a : α} {l : List α} : [a] <+: l ↔ l.head? = some a

theorem List.singleton_prefix_cons_iff {α : Type u_1} {a b : α} {l : List α} : [a] <+: b :: l ↔ a = b

@[simp]

theorem List.singleton_suffix_append_singleton_iff {α : Type u_1} {a b : α} {l : List α} : [a] <:+ l ++ [b] ↔ a = b

@[simp]

theorem List.singleton_suffix_cons_append_singleton_iff {α : Type u_1} {a b c : α} {l : List α} : [a] <:+ b :: (l ++ [c]) ↔ a = c

theorem List.infix_append_iff {α : Type u} {l xs ys : List α} : l <:+: xs ++ ys ↔ l <:+: xs ∨ l <:+: ys ∨ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ l₁ <:+ xs ∧ l₂ <+: ys

theorem List.infix_append_iff_ne_nil {α : Type u} {l xs ys : List α} : l <:+: xs ++ ys ↔ l <:+: xs ∨ l <:+: ys ∨ ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ≠ [] ∧ l₂ ≠ [] ∧ l = l₁ ++ l₂ ∧ l₁ <:+ xs ∧ l₂ <+: ys