Documentation

Init.Data.List.Sublist

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₂) :
theorem List.filterMap_subset {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : αOption β) (H : l₁ 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 lx = 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₂.lengthl₁ = l₂
theorem List.Sublist.eq_of_length_le :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂l₂.length l₁.lengthl₁ = 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

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₂.lengthl₁ = l₂
theorem List.IsPrefix.eq_of_length :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂l₁.length = l₂.lengthl₁ = l₂
theorem List.IsSuffix.eq_of_length :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂l₁.length = l₂.lengthl₁ = l₂
theorem List.prefix_of_prefix_length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <+: l₃l₂ <+: l₃l₁.length l₂.lengthl₁ <+: 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₂.lengthl₁ <:+ 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 Ll <:+: 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 α) :
theorem List.drop_suffix {α : Type u_1} (n : Nat) (l : List α) :
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 α) :
theorem List.drop_subset {α : Type u_1} (n : Nat) (l : List α) :
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₂) :
theorem List.IsSuffix.filter {α : Type u_1} (p : αBool) ⦃l₁ : List α ⦃l₂ : List α (h : l₁ <:+ l₂) :
theorem List.IsInfix.filter {α : Type u_1} (p : αBool) ⦃l₁ : List α ⦃l₂ : List α (h : l₁ <:+: 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
@[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