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.instTransMemSubset {α : Type u_1} : Trans Membership.mem Subset Membership.mem

Equations

• List.instTransMemSubset = { trans := ⋯ }

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

Equations

• List.instTransSubset = { trans := ⋯ }

@[simp]

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₂

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.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₂

@[simp]

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

@[simp]

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

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

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 := ⋯ }

@[simp]

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₂

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.instTransMemSublist {α : Type u_1} : Trans Membership.mem List.Sublist Membership.mem

Equations

• List.instTransMemSublist = { 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.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.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.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'

@[simp]

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

@[simp]

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

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

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.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) ⋯

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

@[simp]

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

@[simp]

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

@[simp]

theorem List.infix_refl {α : 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.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.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

@[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.infix_iff_prefix_suffix {α : 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.IsPrefix.eq_of_length : ∀ {α : 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.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.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₂

@[simp]

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} {a : α} {n : Nat} {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.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₂

@[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) ⋯