Documentation

Mathlib.Data.List.InsertIdx

insertIdx #

Proves various lemmas about List.insertIdx.

source
@[simp]
theorem List.sublist_insertIdx {α : Type u} (l : List α) (n : ℕ) (a : α) :
l.Sublist (l.insertIdx n a)
source
@[simp]
theorem List.subset_insertIdx {α : Type u} (l : List α) (n : ℕ) (a : α) :
l ⊆ l.insertIdx n a
source
@[simp]
theorem List.insertIdx_eraseIdx {α : Type u} {l : List α} {n : ℕ} (hn : n ≠ l.length) (a : α) :
(l.eraseIdx n).insertIdx n a = l.set n a

Erasing nth element of a list, then inserting a at the same place is the same as setting nth element to a.

We assume that n ≠ length l, because otherwise LHS equals l ++ [a] while RHS equals l.

source
theorem List.insertIdx_eraseIdx_getElem {α : Type u} {l : List α} {n : ℕ} (hn : n < l.length) :
(l.eraseIdx n).insertIdx n l[n] = l
source
theorem List.eq_or_mem_of_mem_insertIdx {α : Type u} {l : List α} {n : ℕ} {a b : α} (h : a ∈ l.insertIdx n b) :
a = b ∨ a ∈ l
source
theorem List.insertIdx_subset_cons {α : Type u} (n : ℕ) (a : α) (l : List α) :
l.insertIdx n a ⊆ a :: l
source
theorem List.insertIdx_pmap {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} {a : α} {n : ℕ} (hl : ∀ (x : α), x ∈ l → p x) (ha : p a) :
(pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
source
theorem List.map_insertIdx {α : Type u} {β : Type v} (f : α → β) (l : List α) (n : ℕ) (a : α) :
map f (l.insertIdx n a) = (map f l).insertIdx n (f a)
source
theorem List.eraseIdx_pmap {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (hl : ∀ (a : α), a ∈ l → p a) (n : ℕ) :
(pmap f l hl).eraseIdx n = pmap f (l.eraseIdx n) ⋯
source
theorem List.eraseIdx_map {α : Type u} {β : Type v} (f : α → β) (l : List α) (n : ℕ) :
(map f l).eraseIdx n = map f (l.eraseIdx n)

Erasing an index commutes with List.map.

source
theorem List.get_insertIdx_of_lt {α : Type u} (l : List α) (x : α) (n k : ℕ) (hn : k < n) (hk : k < l.length) (hk' : k < (l.insertIdx n x).length := ⋯) :
(l.insertIdx n x).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩
source
theorem List.get_insertIdx_self {α : Type u} (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length) (hn' : n < (l.insertIdx n x).length := ⋯) :
(l.insertIdx n x).get ⟨n, hn'⟩ = x
source
theorem List.getElem_insertIdx_add_succ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length) (hk : n + k + 1 < (l.insertIdx n x).length := ⋯) :
(l.insertIdx n x)[n + k + 1] = l[n + k]
source
theorem List.get_insertIdx_add_succ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length) (hk : n + k + 1 < (l.insertIdx n x).length := ⋯) :
(l.insertIdx n x).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩
source
theorem List.insertIdx_injective {α : Type u} (n : ℕ) (x : α) :
Function.Injective fun (l : List α) => l.insertIdx n x
source
@[deprecated List.insertIdx_zero (since := "2024-10-21")]
theorem List.insertNth_zero {α : Type u} {xs : List α} {x : α} :
xs.insertIdx 0 x = x :: xs

Alias of List.insertIdx_zero.

source
@[deprecated List.insertIdx_succ_nil (since := "2024-10-21")]
theorem List.insertNth_succ_nil {α : Type u} {n : ℕ} {a : α} :
[].insertIdx (n + 1) a = []

Alias of List.insertIdx_succ_nil.

source
@[deprecated List.insertIdx_succ_cons (since := "2024-10-21")]
theorem List.insertNth_succ_cons {α : Type u} {xs : List α} {hd x : α} {i : ℕ} :
(hd :: xs).insertIdx (i + 1) x = hd :: xs.insertIdx i x

Alias of List.insertIdx_succ_cons.

source
@[deprecated List.length_insertIdx (since := "2024-10-21")]
theorem List.length_insertNth {α : Type u} {a : α} {i : ℕ} {as : List α} :
(as.insertIdx i a).length = if i ≤ as.length then as.length + 1 else as.length

Alias of List.length_insertIdx.

source
@[deprecated List.eraseIdx_insertIdx (since := "2024-10-21")]
theorem List.removeNth_insertIdx {α : Type u} {i : ℕ} {l : List α} (a : α) :
(l.insertIdx i a).eraseIdx i = l

Alias of List.eraseIdx_insertIdx.

source
@[deprecated List.insertIdx_eraseIdx_of_ge (since := "2024-10-21")]
theorem List.insertNth_eraseIdx_of_ge {α : Type u} {a : α} {i m : ℕ} {as : List α} :
i < as.length → i ≤ m → (as.eraseIdx i).insertIdx m a = (as.insertIdx (m + 1) a).eraseIdx i

Alias of List.insertIdx_eraseIdx_of_ge.

source
@[deprecated List.insertIdx_eraseIdx_of_le (since := "2024-10-21")]
theorem List.insertNth_eraseIdx_of_le {α : Type u} {a : α} {i j : ℕ} {as : List α} :
i < as.length → j ≤ i → (as.eraseIdx i).insertIdx j a = (as.insertIdx j a).eraseIdx (i + 1)

Alias of List.insertIdx_eraseIdx_of_le.

source
@[deprecated List.insertIdx_comm (since := "2024-10-21")]
theorem List.insertNth_comm {α : Type u} (a b : α) {i j : ℕ} {l : List α} :
i ≤ j → j ≤ l.length → (l.insertIdx i a).insertIdx (j + 1) b = (l.insertIdx j b).insertIdx i a

Alias of List.insertIdx_comm.

source
@[deprecated List.mem_insertIdx (since := "2024-10-21")]
theorem List.mem_insertNth {α : Type u} {a b : α} {i : ℕ} {l : List α} :
i ≤ l.length → (a ∈ l.insertIdx i b ↔ a = b ∨ a ∈ l)

Alias of List.mem_insertIdx.

source
@[deprecated List.insertIdx_of_length_lt (since := "2024-10-21")]
theorem List.insertNth_of_length_lt {α : Type u} {l : List α} {x : α} {i : ℕ} (h : l.length < i) :
l.insertIdx i x = l

Alias of List.insertIdx_of_length_lt.

source
@[deprecated List.insertIdx_length_self (since := "2024-10-21")]
theorem List.insertNth_length_self {α : Type u} {l : List α} {x : α} :
l.insertIdx l.length x = l ++ [x]

Alias of List.insertIdx_length_self.

source
@[deprecated List.length_le_length_insertIdx (since := "2024-10-21")]
theorem List.length_le_length_insertNth {α : Type u} {l : List α} {x : α} {i : ℕ} :
l.length ≤ (l.insertIdx i x).length

Alias of List.length_le_length_insertIdx.

source
@[deprecated List.length_insertIdx_le_succ (since := "2024-10-21")]
theorem List.length_insertNth_le_succ {α : Type u} {l : List α} {x : α} {i : ℕ} :
(l.insertIdx i x).length ≤ l.length + 1

Alias of List.length_insertIdx_le_succ.

source
@[deprecated List.getElem_insertIdx_of_lt (since := "2024-10-21")]
theorem List.getElem_insertNth_of_lt {α : Type u} {l : List α} {x : α} {i j : ℕ} (hn : j < i) (hk : j < (l.insertIdx i x).length) :
(l.insertIdx i x)[j] = l[j]

Alias of List.getElem_insertIdx_of_lt.

source
@[deprecated List.get_insertIdx_of_lt (since := "2024-10-21")]
theorem List.get_insertNth_of_lt {α : Type u} (l : List α) (x : α) (n k : ℕ) (hn : k < n) (hk : k < l.length) (hk' : k < (l.insertIdx n x).length := ⋯) :
(l.insertIdx n x).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩

Alias of List.get_insertIdx_of_lt.

source
@[deprecated List.getElem_insertIdx_self (since := "2024-10-21")]
theorem List.getElem_insertNth_self {α : Type u} {l : List α} {x : α} {i : ℕ} (hi : i < (l.insertIdx i x).length) :
(l.insertIdx i x)[i] = x

Alias of List.getElem_insertIdx_self.

source
@[deprecated List.get_insertIdx_self (since := "2024-10-21")]
theorem List.get_insertNth_self {α : Type u} (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length) (hn' : n < (l.insertIdx n x).length := ⋯) :
(l.insertIdx n x).get ⟨n, hn'⟩ = x

Alias of List.get_insertIdx_self.

source
@[deprecated List.getElem_insertIdx_add_succ (since := "2024-10-21")]
theorem List.getElem_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length) (hk : n + k + 1 < (l.insertIdx n x).length := ⋯) :
(l.insertIdx n x)[n + k + 1] = l[n + k]

Alias of List.getElem_insertIdx_add_succ.

source
@[deprecated List.get_insertIdx_add_succ (since := "2024-10-21")]
theorem List.get_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length) (hk : n + k + 1 < (l.insertIdx n x).length := ⋯) :
(l.insertIdx n x).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩

Alias of List.get_insertIdx_add_succ.

source
@[deprecated List.insertIdx_injective (since := "2024-10-21")]
theorem List.insertNth_injective {α : Type u} (n : ℕ) (x : α) :
Function.Injective fun (l : List α) => l.insertIdx n x

Alias of List.insertIdx_injective.