Documentation

Init.Data.List.Nat.Sublist

Further lemmas about List.IsSuffix / List.IsPrefix / List.IsInfix. #

These are in a separate file from most of the lemmas about List.IsSuffix as they required importing more lemmas about natural numbers, and use omega.

theorem List.IsSuffix.getElem {α : Type u_1} {x : List α} {y : List α} (h : x <:+ y) {n : Nat} (hn : n < x.length) :
x[n] = y[y.length - x.length + n]
theorem List.isSuffix_iff :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ l₁.length l₂.length ∀ (i : Nat) (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]
theorem List.isInfix_iff :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ ∃ (k : Nat), l₁.length + k l₂.length ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
theorem List.suffix_iff_eq_append :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ List.take (l₂.length - l₁.length) l₂ ++ l₁ = l₂
theorem List.prefix_take_iff {α : Type u_1} {x : List α} {y : List α} {n : Nat} :
x <+: List.take n y x <+: y x.length n
theorem List.suffix_iff_eq_drop :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ l₁ = List.drop (l₂.length - l₁.length) l₂
theorem List.prefix_take_le_iff {α : Type u_1} {m : Nat} {n : Nat} {L : List α} (hm : m < L.length) :
@[simp]
theorem List.append_left_sublist_self {α : Type u_1} {xs : List α} (ys : List α) :
(xs ++ ys).Sublist ys xs = []
@[simp]
theorem List.append_right_sublist_self {α : Type u_1} (xs : List α) {ys : List α} :
(xs ++ ys).Sublist xs ys = []
theorem List.append_sublist_of_sublist_left {α : Type u_1} {xs : List α} {ys : List α} {zs : List α} (h : zs.Sublist xs) :
(xs ++ ys).Sublist zs ys = [] xs = zs
theorem List.append_sublist_of_sublist_right {α : Type u_1} {xs : List α} {ys : List α} {zs : List α} (h : zs.Sublist ys) :
(xs ++ ys).Sublist zs xs = [] ys = zs