Basic properties of List.eraseIdx

List.eraseIdx l k erases k-th element of l : List α. If k ≥ length l, then it returns l.

@[simp]

theorem List.eraseIdx_zero {α : Type u} (l : List α) : l.eraseIdx 0 = l.tail

theorem List.eraseIdx_eq_take_drop_succ {α : Type u} (l : List α) (i : Nat) : l.eraseIdx i = List.take i l ++ List.drop (i + 1) l

theorem List.eraseIdx_sublist {α : Type u} (l : List α) (k : Nat) : (l.eraseIdx k).Sublist l

theorem List.eraseIdx_subset {α : Type u} (l : List α) (k : Nat) : l.eraseIdx k ⊆ l

@[simp]

theorem List.eraseIdx_eq_self {α : Type u} {l : List α} {k : Nat} : l.eraseIdx k = l ↔ l.length ≤ k

theorem List.eraseIdx_of_length_le {α : Type u} {l : List α} {k : Nat} : l.length ≤ k → l.eraseIdx k = l

Alias of the reverse direction of List.eraseIdx_eq_self.

theorem List.eraseIdx_append_of_lt_length {α : Type u} {l : List α} {k : Nat} (hk : k < l.length) (l' : List α) : (l ++ l').eraseIdx k = l.eraseIdx k ++ l'

theorem List.eraseIdx_append_of_length_le {α : Type u} {l : List α} {k : Nat} (hk : l.length ≤ k) (l' : List α) : (l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)

theorem List.IsPrefix.eraseIdx {α : Type u} {l : List α} {l' : List α} (h : l <+: l') (k : Nat) : l.eraseIdx k <+: l'.eraseIdx k

theorem List.mem_eraseIdx_iff_get {α : Type u} {x : α} {l : List α} {k : Nat} : x ∈ l.eraseIdx k ↔ ∃ (i : Fin l.length), ↑i ≠ k ∧ l.get i = x

theorem List.mem_eraseIdx_iff_get? {α : Type u} {x : α} {l : List α} {k : Nat} : x ∈ l.eraseIdx k ↔ ∃ (i : Nat), i ≠ k ∧ l.get? i = some x