insertIdx #
Proves various lemmas about List.insertIdx.
@[simp]
theorem
List.sublist_insertIdx
{α : Type u}
(l : List α)
(n : ℕ)
(a : α)
:
l.Sublist (l.insertIdx n a)
@[simp]
@[simp]
theorem
List.insertIdx_eraseIdx_self
{α : 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.
theorem
List.insertIdx_eraseIdx_getElem
{α : Type u}
{l : List α}
{n : ℕ}
(hn : n < l.length)
:
(l.eraseIdx n).insertIdx n l[n] = l
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
theorem
List.insertIdx_subset_cons
{α : Type u}
(n : ℕ)
(a : α)
(l : List α)
:
l.insertIdx n a ⊆ a :: l
theorem
List.insertIdx_pmap
{α : Type u}
{β : Type v}
{p : α → Prop}
(f : (a : α) → p a → β)
{l : List α}
{a : α}
{n : ℕ}
(hl : ∀ x ∈ l, p x)
(ha : p a)
:
(pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
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)
theorem
List.eraseIdx_pmap
{α : Type u}
{β : Type v}
{p : α → Prop}
(f : (a : α) → p a → β)
{l : List α}
(hl : ∀ a ∈ l, p a)
(n : ℕ)
:
(pmap f l hl).eraseIdx n = pmap f (l.eraseIdx n) ⋯
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.
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
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]
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'⟩
theorem
List.insertIdx_injective
{α : Type u}
(n : ℕ)
(x : α)
:
Function.Injective fun (l : List α) => l.insertIdx n x
theorem
List.take_insertIdx_eq_take_of_le
{α : Type u}
(l : List α)
(x : α)
(i j : ℕ)
(h : i ≤ j)
:
take i (l.insertIdx j x) = take i l
theorem
List.take_eraseIdx_eq_take_of_le
{α : Type u}
(l : List α)
(i j : ℕ)
(h : i ≤ j)
:
take i (l.eraseIdx j) = take i l