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} {xs ys : List α} (h : xs <:+ ys) {i : Nat} (hn : i < xs.length) :
xs[i] = ys[ys.length - xs.length + i]
theorem List.suffix_iff_getElem? {α✝ : 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]
@[reducible, inline, deprecated List.suffix_iff_getElem? (since := "2025-05-27")]
abbrev 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]
Equations
    Instances For
      theorem List.suffix_iff_getElem {α : Type u_1} {l₁ l₂ : List α} :
      l₁ <:+ l₂ (x : l₁.length l₂.length), ∀ (i : Nat) (x_1 : i < l₁.length), l₂[i + l₂.length - l₁.length] = l₁[i]
      theorem List.infix_iff_getElem? {α✝ : 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]
      @[reducible, inline, deprecated List.infix_iff_getElem? (since := "2025-05-27")]
      abbrev 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]
      Equations
        Instances For
          theorem List.suffix_iff_eq_append {α✝ : Type u_1} {l₁ l₂ : List α✝} :
          l₁ <:+ l₂ take (l₂.length - l₁.length) l₂ ++ l₁ = l₂
          theorem List.prefix_take_iff {α : Type u_1} {xs ys : List α} {i : Nat} :
          xs <+: take i ys xs <+: ys xs.length i
          theorem List.suffix_iff_eq_drop {α✝ : Type u_1} {l₁ l₂ : List α✝} :
          l₁ <:+ l₂ l₁ = drop (l₂.length - l₁.length) l₂
          theorem List.prefix_take_le_iff {α : Type u_1} {i j : Nat} {xs : List α} (hm : i < xs.length) :
          take i xs <+: take j xs i j
          @[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 ys zs : List α} (h : zs.Sublist xs) :
          (xs ++ ys).Sublist zs ys = [] xs = zs
          theorem List.append_sublist_of_sublist_right {α : Type u_1} {xs ys zs : List α} (h : zs.Sublist ys) :
          (xs ++ ys).Sublist zs xs = [] ys = zs