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.

source
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]
source
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]
source
@[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
    source
    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]
    source
    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]
    source
    @[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
      source
      theorem List.suffix_iff_eq_append {α✝ : Type u_1} {l₁ l₂ : List α✝} :
      l₁ <:+ l₂ ↔ take (l₂.length - l₁.length) l₂ ++ l₁ = l₂
      source
      theorem List.prefix_take_iff {α : Type u_1} {xs ys : List α} {i : Nat} :
      xs <+: take i ys ↔ xs <+: ys ∧ xs.length ≤ i
      source
      theorem List.suffix_iff_eq_drop {α✝ : Type u_1} {l₁ l₂ : List α✝} :
      l₁ <:+ l₂ ↔ l₁ = drop (l₂.length - l₁.length) l₂
      source
      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
      source
      @[simp]
      theorem List.append_left_sublist_self {α : Type u_1} {xs : List α} (ys : List α) :
      (xs ++ ys).Sublist ys ↔ xs = []
      source
      @[simp]
      theorem List.append_right_sublist_self {α : Type u_1} (xs : List α) {ys : List α} :
      (xs ++ ys).Sublist xs ↔ ys = []
      source
      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
      source
      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