insertNth #
Proves various lemmas about List.insertNth.
@[simp]
@[simp]
@[simp]
theorem
List.insertNth_succ_cons
{α : Type u}
(s : List α)
(hd : α)
(x : α)
(n : ℕ)
:
List.insertNth (n + 1) x (hd :: s) = hd :: List.insertNth n x s
theorem
List.length_insertNth
{α : Type u}
{a : α}
(n : ℕ)
(as : List α)
:
n ≤ as.length → (List.insertNth n a as).length = as.length + 1
theorem
List.eraseIdx_insertNth
{α : Type u}
{a : α}
(n : ℕ)
(l : List α)
:
(List.insertNth n a l).eraseIdx n = l
@[deprecated List.eraseIdx_insertNth]
theorem
List.removeNth_insertNth
{α : Type u}
{a : α}
(n : ℕ)
(l : List α)
:
(List.insertNth n a l).eraseIdx n = l
Alias of List.eraseIdx_insertNth.
theorem
List.insertNth_eraseIdx_of_ge
{α : Type u}
{a : α}
(n : ℕ)
(m : ℕ)
(as : List α)
:
n < as.length → n ≤ m → List.insertNth m a (as.eraseIdx n) = (List.insertNth (m + 1) a as).eraseIdx n
@[deprecated List.insertNth_eraseIdx_of_ge]
theorem
List.insertNth_removeNth_of_ge
{α : Type u}
{a : α}
(n : ℕ)
(m : ℕ)
(as : List α)
:
n < as.length → n ≤ m → List.insertNth m a (as.eraseIdx n) = (List.insertNth (m + 1) a as).eraseIdx n
Alias of List.insertNth_eraseIdx_of_ge.
theorem
List.insertNth_eraseIdx_of_le
{α : Type u}
{a : α}
(n : ℕ)
(m : ℕ)
(as : List α)
:
n < as.length → m ≤ n → List.insertNth m a (as.eraseIdx n) = (List.insertNth m a as).eraseIdx (n + 1)
@[deprecated List.insertNth_eraseIdx_of_le]
theorem
List.insertNth_removeNth_of_le
{α : Type u}
{a : α}
(n : ℕ)
(m : ℕ)
(as : List α)
:
n < as.length → m ≤ n → List.insertNth m a (as.eraseIdx n) = (List.insertNth m a as).eraseIdx (n + 1)
Alias of List.insertNth_eraseIdx_of_le.
theorem
List.insertNth_comm
{α : Type u}
(a : α)
(b : α)
(i : ℕ)
(j : ℕ)
(l : List α)
:
i ≤ j → j ≤ l.length → List.insertNth (j + 1) b (List.insertNth i a l) = List.insertNth i a (List.insertNth j b l)
theorem
List.insertNth_of_length_lt
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
(h : l.length < n)
:
List.insertNth n x l = l
@[simp]
theorem
List.insertNth_length_self
{α : Type u}
(l : List α)
(x : α)
:
List.insertNth l.length x l = l ++ [x]
theorem
List.length_le_length_insertNth
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
:
l.length ≤ (List.insertNth n x l).length
theorem
List.length_insertNth_le_succ
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
:
(List.insertNth n x l).length ≤ l.length + 1
theorem
List.getElem_insertNth_of_lt
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
(k : ℕ)
(hn : k < n)
(hk : k < l.length)
(hk' : optParam (k < (List.insertNth n x l).length) ⋯)
:
(List.insertNth n x l)[k] = l[k]
theorem
List.get_insertNth_of_lt
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
(k : ℕ)
(hn : k < n)
(hk : k < l.length)
(hk' : optParam (k < (List.insertNth n x l).length) ⋯)
:
(List.insertNth n x l).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩
@[deprecated List.get_insertNth_of_lt]
theorem
List.nthLe_insertNth_of_lt
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
(k : ℕ)
:
k < n →
∀ (hk : k < l.length) (hk' : optParam (k < (List.insertNth n x l).length) ⋯),
(List.insertNth n x l).nthLe k hk' = l.nthLe k hk
@[simp]
theorem
List.getElem_insertNth_self
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
(hn : n ≤ l.length)
(hn' : optParam (n < (List.insertNth n x l).length) ⋯)
:
(List.insertNth n x l)[n] = x
theorem
List.get_insertNth_self
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
(hn : n ≤ l.length)
(hn' : optParam (n < (List.insertNth n x l).length) ⋯)
:
(List.insertNth n x l).get ⟨n, hn'⟩ = x
@[simp, deprecated List.get_insertNth_self]
theorem
List.nthLe_insertNth_self
{α : Type u}
(l : List α)
(x : α)
(n : ℕ)
(hn : n ≤ l.length)
(hn' : optParam (n < (List.insertNth n x l).length) ⋯)
:
(List.insertNth n x l).nthLe n hn' = x