Documentation

Mathlib.Data.List.InsertIdx

insertIdx #

Proves various lemmas about List.insertIdx.

@[simp]
theorem List.insertIdx_zero {α : Type u} (s : List α) (x : α) :
List.insertIdx 0 x s = x :: s
@[simp]
theorem List.insertIdx_succ_nil {α : Type u} (n : ) (a : α) :
List.insertIdx (n + 1) a [] = []
@[simp]
theorem List.insertIdx_succ_cons {α : Type u} (s : List α) (hd : α) (x : α) (n : ) :
List.insertIdx (n + 1) x (hd :: s) = hd :: List.insertIdx n x s
theorem List.length_insertIdx {α : Type u} {a : α} (n : ) (as : List α) :
n as.length(List.insertIdx n a as).length = as.length + 1
theorem List.eraseIdx_insertIdx {α : Type u} {a : α} (n : ) (l : List α) :
(List.insertIdx n a l).eraseIdx n = l
theorem List.insertIdx_eraseIdx_of_ge {α : Type u} {a : α} (n : ) (m : ) (as : List α) :
n < as.lengthn mList.insertIdx m a (as.eraseIdx n) = (List.insertIdx (m + 1) a as).eraseIdx n
theorem List.insertIdx_eraseIdx_of_le {α : Type u} {a : α} (n : ) (m : ) (as : List α) :
n < as.lengthm nList.insertIdx m a (as.eraseIdx n) = (List.insertIdx m a as).eraseIdx (n + 1)
theorem List.insertIdx_comm {α : Type u} (a : α) (b : α) (i : ) (j : ) (l : List α) :
i jj l.lengthList.insertIdx (j + 1) b (List.insertIdx i a l) = List.insertIdx i a (List.insertIdx j b l)
theorem List.mem_insertIdx {α : Type u} {a : α} {b : α} {n : } {l : List α} :
n l.length(a List.insertIdx n b l a = b a l)
theorem List.insertIdx_of_length_lt {α : Type u} (l : List α) (x : α) (n : ) (h : l.length < n) :
@[simp]
theorem List.insertIdx_length_self {α : Type u} (l : List α) (x : α) :
List.insertIdx l.length x l = l ++ [x]
theorem List.length_le_length_insertIdx {α : Type u} (l : List α) (x : α) (n : ) :
l.length (List.insertIdx n x l).length
theorem List.length_insertIdx_le_succ {α : Type u} (l : List α) (x : α) (n : ) :
(List.insertIdx n x l).length l.length + 1
theorem List.getElem_insertIdx_of_lt {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hn : k < n) (hk : k < l.length) (hk' : optParam (k < (List.insertIdx n x l).length) ) :
(List.insertIdx n x l)[k] = l[k]
theorem List.get_insertIdx_of_lt {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hn : k < n) (hk : k < l.length) (hk' : optParam (k < (List.insertIdx n x l).length) ) :
(List.insertIdx n x l).get k, hk' = l.get k, hk
@[simp]
theorem List.getElem_insertIdx_self {α : Type u} (l : List α) (x : α) (n : ) (hn : n l.length) (hn' : optParam (n < (List.insertIdx n x l).length) ) :
(List.insertIdx n x l)[n] = x
theorem List.get_insertIdx_self {α : Type u} (l : List α) (x : α) (n : ) (hn : n l.length) (hn' : optParam (n < (List.insertIdx n x l).length) ) :
(List.insertIdx n x l).get n, hn' = x
theorem List.getElem_insertIdx_add_succ {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hk' : n + k < l.length) (hk : optParam (n + k + 1 < (List.insertIdx n x l).length) ) :
(List.insertIdx n x l)[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 : optParam (n + k + 1 < (List.insertIdx n x l).length) ) :
(List.insertIdx n x l).get n + k + 1, hk = l.get n + k, hk'
@[deprecated List.insertIdx_zero]
theorem List.insertNth_zero {α : Type u} (s : List α) (x : α) :
List.insertIdx 0 x s = x :: s

Alias of List.insertIdx_zero.

@[deprecated List.insertIdx_succ_nil]
theorem List.insertNth_succ_nil {α : Type u} (n : ) (a : α) :
List.insertIdx (n + 1) a [] = []

Alias of List.insertIdx_succ_nil.

@[deprecated List.insertIdx_succ_cons]
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]
theorem List.length_insertNth {α : Type u} {a : α} (n : ) (as : List α) :
n as.length(List.insertIdx n a as).length = as.length + 1

Alias of List.length_insertIdx.

@[deprecated List.eraseIdx_insertIdx]
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]
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]
theorem List.insertNth_eraseIdx_of_ge {α : Type u} {a : α} (n : ) (m : ) (as : List α) :
n < as.lengthn mList.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]
theorem List.insertNth_removeNth_of_ge {α : Type u} {a : α} (n : ) (m : ) (as : List α) :
n < as.lengthn mList.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]
theorem List.insertNth_eraseIdx_of_le {α : Type u} {a : α} (n : ) (m : ) (as : List α) :
n < as.lengthm nList.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]
theorem List.insertIdx_removeNth_of_le {α : Type u} {a : α} (n : ) (m : ) (as : List α) :
n < as.lengthm nList.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]
theorem List.insertNth_comm {α : Type u} (a : α) (b : α) (i : ) (j : ) (l : List α) :
i jj l.lengthList.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]
theorem List.mem_insertNth {α : Type u} {a : α} {b : α} {n : } {l : List α} :
n l.length(a List.insertIdx n b l a = b a l)

Alias of List.mem_insertIdx.

@[deprecated List.insertIdx_of_length_lt]
theorem List.insertNth_of_length_lt {α : Type u} (l : List α) (x : α) (n : ) (h : l.length < n) :

Alias of List.insertIdx_of_length_lt.

@[deprecated List.insertIdx_length_self]
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]
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]
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]
theorem List.getElem_insertNth_of_lt {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hn : k < n) (hk : k < l.length) (hk' : optParam (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]
theorem List.get_insertNth_of_lt {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hn : k < n) (hk : k < l.length) (hk' : optParam (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]
theorem List.getElem_insertNth_self {α : Type u} (l : List α) (x : α) (n : ) (hn : n l.length) (hn' : optParam (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]
theorem List.get_insertNth_self {α : Type u} (l : List α) (x : α) (n : ) (hn : n l.length) (hn' : optParam (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]
theorem List.getElem_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hk' : n + k < l.length) (hk : optParam (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]
theorem List.get_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hk' : n + k < l.length) (hk : optParam (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]
theorem List.insertNth_injective {α : Type u} (n : ) (x : α) :

Alias of List.insertIdx_injective.