insertIdx #
Proves various lemmas about List.insertIdx.
theorem
List.get_insertIdx_of_lt
{α : Type u}
(l : List α)
(x : α)
(n k : ℕ)
(hn : k < n)
(hk : k < l.length)
(hk' : k < (List.insertIdx n x l).length := ⋯)
:
(List.insertIdx n x l).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩
theorem
List.get_insertIdx_self
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
(hn : n ≤ l.length)
(hn' : n < (List.insertIdx n x l).length := ⋯)
:
(List.insertIdx n x l).get ⟨n, hn'⟩ = x
@[deprecated List.insertIdx_zero (since := "2024-10-21")]
Alias of List.insertIdx_zero.
@[deprecated List.insertIdx_succ_nil (since := "2024-10-21")]
Alias of List.insertIdx_succ_nil.
@[deprecated List.insertIdx_succ_cons (since := "2024-10-21")]
theorem
List.insertNth_succ_cons
{α : Type u}
(s : List α)
(hd x : α)
(n : ℕ)
:
List.insertIdx (n + 1) x (hd :: s) = hd :: List.insertIdx n x s
Alias of List.insertIdx_succ_cons.
@[deprecated List.length_insertIdx (since := "2024-10-21")]
theorem
List.length_insertNth
{α : Type u}
{a : α}
(n : ℕ)
(as : List α)
:
(List.insertIdx n a as).length = if n ≤ as.length then as.length + 1 else as.length
Alias of List.length_insertIdx.
@[deprecated List.eraseIdx_insertIdx (since := "2024-10-21")]
theorem
List.removeNth_insertIdx
{α : Type u}
{a : α}
(n : ℕ)
(l : List α)
:
(List.insertIdx n a l).eraseIdx n = l
Alias of List.eraseIdx_insertIdx.
@[deprecated List.eraseIdx_insertIdx (since := "2024-05-04")]
theorem
List.removeNth_insertNth
{α : Type u}
{a : α}
(n : ℕ)
(l : List α)
:
(List.insertIdx n a l).eraseIdx n = l
Alias of List.eraseIdx_insertIdx.
@[deprecated List.insertIdx_eraseIdx_of_ge (since := "2024-10-21")]
theorem
List.insertNth_eraseIdx_of_ge
{α : Type u}
{a : α}
(n m : ℕ)
(as : List α)
:
n < as.length → n ≤ m → List.insertIdx m a (as.eraseIdx n) = (List.insertIdx (m + 1) a as).eraseIdx n
Alias of List.insertIdx_eraseIdx_of_ge.
@[deprecated List.insertIdx_eraseIdx_of_ge (since := "2024-05-04")]
theorem
List.insertNth_removeNth_of_ge
{α : Type u}
{a : α}
(n m : ℕ)
(as : List α)
:
n < as.length → n ≤ m → List.insertIdx m a (as.eraseIdx n) = (List.insertIdx (m + 1) a as).eraseIdx n
Alias of List.insertIdx_eraseIdx_of_ge.
@[deprecated List.insertIdx_eraseIdx_of_le (since := "2024-10-21")]
theorem
List.insertNth_eraseIdx_of_le
{α : Type u}
{a : α}
(n m : ℕ)
(as : List α)
:
n < as.length → m ≤ n → List.insertIdx m a (as.eraseIdx n) = (List.insertIdx m a as).eraseIdx (n + 1)
Alias of List.insertIdx_eraseIdx_of_le.
@[deprecated List.insertIdx_eraseIdx_of_le (since := "2024-05-04")]
theorem
List.insertIdx_removeNth_of_le
{α : Type u}
{a : α}
(n m : ℕ)
(as : List α)
:
n < as.length → m ≤ n → List.insertIdx m a (as.eraseIdx n) = (List.insertIdx m a as).eraseIdx (n + 1)
Alias of List.insertIdx_eraseIdx_of_le.
@[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 → List.insertIdx (j + 1) b (List.insertIdx i a l) = List.insertIdx i a (List.insertIdx j b l)
Alias of List.insertIdx_comm.
@[deprecated List.mem_insertIdx (since := "2024-10-21")]
Alias of List.mem_insertIdx.
@[deprecated List.insertIdx_of_length_lt (since := "2024-10-21")]
theorem
List.insertNth_of_length_lt
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
(h : l.length < n)
:
List.insertIdx n x l = l
Alias of List.insertIdx_of_length_lt.
@[deprecated List.insertIdx_length_self (since := "2024-10-21")]
theorem
List.insertNth_length_self
{α : Type u}
(l : List α)
(x : α)
:
List.insertIdx l.length x l = l ++ [x]
Alias of List.insertIdx_length_self.
@[deprecated List.length_le_length_insertIdx (since := "2024-10-21")]
theorem
List.length_le_length_insertNth
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
:
l.length ≤ (List.insertIdx n x l).length
Alias of List.length_le_length_insertIdx.
@[deprecated List.length_insertIdx_le_succ (since := "2024-10-21")]
theorem
List.length_insertNth_le_succ
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
:
(List.insertIdx n x l).length ≤ l.length + 1
Alias of List.length_insertIdx_le_succ.
@[deprecated List.getElem_insertIdx_of_lt (since := "2024-10-21")]
theorem
List.getElem_insertNth_of_lt
{α : Type u}
{l : List α}
{x : α}
{n k : ℕ}
(hn : k < n)
(hk : k < (List.insertIdx n x l).length)
:
(List.insertIdx n x l)[k] = l[k]
Alias of List.getElem_insertIdx_of_lt.
@[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 < (List.insertIdx n x l).length := ⋯)
:
(List.insertIdx n x l).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩
Alias of List.get_insertIdx_of_lt.
@[deprecated List.getElem_insertIdx_self (since := "2024-10-21")]
theorem
List.getElem_insertNth_self
{α : Type u}
{l : List α}
{x : α}
{n : ℕ}
(hn : n < (List.insertIdx n x l).length)
:
(List.insertIdx n x l)[n] = x
Alias of List.getElem_insertIdx_self.
@[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 < (List.insertIdx n x l).length := ⋯)
:
(List.insertIdx n x l).get ⟨n, hn'⟩ = x
Alias of List.get_insertIdx_self.
@[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 < (List.insertIdx n x l).length := ⋯)
:
(List.insertIdx n x l)[n + k + 1] = l[n + k]
Alias of List.getElem_insertIdx_add_succ.
@[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 < (List.insertIdx n x l).length := ⋯)
:
(List.insertIdx n x l).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩
Alias of List.get_insertIdx_add_succ.
@[deprecated List.insertIdx_injective (since := "2024-10-21")]
Alias of List.insertIdx_injective.