Documentation

Init.Data.List.Nat.InsertIdx

insertIdx #

Proves various lemmas about List.insertIdx.

source
@[simp]
theorem List.insertIdx_zero {α : Type u} {xs : List α} {x : α} :
xs.insertIdx 0 x = x :: xs
source
@[simp]
theorem List.insertIdx_succ_nil {α : Type u} {n : Nat} {a : α} :
[].insertIdx (n + 1) a = []
source
@[simp]
theorem List.insertIdx_succ_cons {α : Type u} {xs : List α} {hd x : α} {i : Nat} :
(hd :: xs).insertIdx (i + 1) x = hd :: xs.insertIdx i x
source
theorem List.length_insertIdx {α : Type u} {a : α} {i : Nat} {as : List α} :
(as.insertIdx i a).length = if i ≤ as.length then as.length + 1 else as.length
source
theorem List.length_insertIdx_of_le_length {α : Type u} {i : Nat} {as : List α} (h : i ≤ as.length) (a : α) :
(as.insertIdx i a).length = as.length + 1
source
theorem List.length_insertIdx_of_length_lt {α : Type u} {as : List α} {i : Nat} (h : as.length < i) (a : α) :
(as.insertIdx i a).length = as.length
source
theorem List.insertIdx_eraseIdx_of_ge {α : Type u} {a : α} {i j : Nat} {as : List α} :
i < as.length → i ≤ j → (as.eraseIdx i).insertIdx j a = (as.insertIdx (j + 1) a).eraseIdx i
source
theorem List.insertIdx_eraseIdx_of_le {α : Type u} {a : α} {i j : Nat} {as : List α} :
i < as.length → j ≤ i → (as.eraseIdx i).insertIdx j a = (as.insertIdx j a).eraseIdx (i + 1)
source
theorem List.insertIdx_eraseIdx {α : Type u} {a : α} {i : Nat} {as : List α} {j : Nat} (h : i < as.length) :
(as.eraseIdx i).insertIdx j a = if i ≤ j then (as.insertIdx (j + 1) a).eraseIdx i else (as.insertIdx j a).eraseIdx (i + 1)
source
theorem List.insertIdx_comm {α : Type u} (a b : α) {i j : Nat} {l : List α} :
i ≤ j → j ≤ l.length → (l.insertIdx i a).insertIdx (j + 1) b = (l.insertIdx j b).insertIdx i a
source
theorem List.mem_insertIdx {α : Type u} {a b : α} {i : Nat} {l : List α} :
i ≤ l.length → (a ∈ l.insertIdx i b ↔ a = b ∨ a ∈ l)
source
theorem List.insertIdx_of_length_lt {α : Type u} {l : List α} {x : α} {i : Nat} (h : l.length < i) :
l.insertIdx i x = l
source
@[simp]
theorem List.eraseIdx_insertIdx_self {α : Type u} {i : Nat} {l : List α} (a : α) :
(l.insertIdx i a).eraseIdx i = l
source
@[reducible, inline, deprecated List.eraseIdx_insertIdx_self (since := "2025-06-18")]
abbrev List.eraseIdx_insertIdx {α : Type u_1} {i : Nat} {l : List α} (a : α) :
(l.insertIdx i a).eraseIdx i = l
Equations
Instances For
    source
    @[simp]
    theorem List.insertIdx_length_self {α : Type u} {l : List α} {x : α} :
    l.insertIdx l.length x = l ++ [x]
    source
    theorem List.length_le_length_insertIdx {α : Type u} {l : List α} {x : α} {i : Nat} :
    l.length ≤ (l.insertIdx i x).length
    source
    theorem List.length_insertIdx_le_succ {α : Type u} {l : List α} {x : α} {i : Nat} :
    (l.insertIdx i x).length ≤ l.length + 1
    source
    theorem List.getElem_insertIdx_of_lt {α : Type u} {l : List α} {x : α} {i j : Nat} (hn : j < i) (hk : j < (l.insertIdx i x).length) :
    (l.insertIdx i x)[j] = l[j]
    source
    @[simp]
    theorem List.getElem_insertIdx_self {α : Type u} {l : List α} {x : α} {i : Nat} (hi : i < (l.insertIdx i x).length) :
    (l.insertIdx i x)[i] = x
    source
    theorem List.getElem_insertIdx_of_gt {α : Type u} {l : List α} {x : α} {i j : Nat} (hn : i < j) (hk : j < (l.insertIdx i x).length) :
    (l.insertIdx i x)[j] = l[j - 1]
    source
    @[reducible, inline, deprecated List.getElem_insertIdx_of_gt (since := "2025-02-04")]
    abbrev List.getElem_insertIdx_of_ge {α : Type u_1} {l : List α} {x : α} {i j : Nat} (hn : i < j) (hk : j < (l.insertIdx i x).length) :
    (l.insertIdx i x)[j] = l[j - 1]
    Equations
    Instances For
      source
      theorem List.getElem_insertIdx {α : Type u} {l : List α} {x : α} {i j : Nat} (h : j < (l.insertIdx i x).length) :
      (l.insertIdx i x)[j] = if h₁ : j < i then l[j] else if h₂ : j = i then x else l[j - 1]
      source
      theorem List.getElem?_insertIdx {α : Type u} {l : List α} {x : α} {i j : Nat} :
      (l.insertIdx i x)[j]? = if j < i then l[j]? else if j = i then if j ≤ l.length then some x else none else l[j - 1]?
      source
      theorem List.getElem?_insertIdx_of_lt {α : Type u} {l : List α} {x : α} {i j : Nat} (h : j < i) :
      (l.insertIdx i x)[j]? = l[j]?
      source
      theorem List.getElem?_insertIdx_self {α : Type u} {l : List α} {x : α} {i : Nat} :
      (l.insertIdx i x)[i]? = if i ≤ l.length then some x else none
      source
      theorem List.getElem?_insertIdx_of_gt {α : Type u} {l : List α} {x : α} {i j : Nat} (h : i < j) :
      (l.insertIdx i x)[j]? = l[j - 1]?
      source
      @[reducible, inline, deprecated List.getElem?_insertIdx_of_gt (since := "2025-02-04")]
      abbrev List.getElem?_insertIdx_of_ge {α : Type u_1} {l : List α} {x : α} {i j : Nat} (h : i < j) :
      (l.insertIdx i x)[j]? = l[j - 1]?
      Equations
      Instances For