Documentation

Init.Data.List.Erase

Lemmas about List.eraseP and List.erase. #

eraseP #

@[simp]
theorem List.eraseP_nil :
∀ {α : Type u_1} {p : αBool}, List.eraseP p [] = []
theorem List.eraseP_cons {α : Type u_1} {p : αBool} (a : α) (l : List α) :
List.eraseP p (a :: l) = bif p a then l else a :: List.eraseP p l
@[simp]
theorem List.eraseP_cons_of_pos {α : Type u_1} {a : α} {l : List α} {p : αBool} (h : p a = true) :
List.eraseP p (a :: l) = l
@[simp]
theorem List.eraseP_cons_of_neg {α : Type u_1} {a : α} {l : List α} {p : αBool} (h : ¬p a = true) :
List.eraseP p (a :: l) = a :: List.eraseP p l
theorem List.eraseP_of_forall_not {α : Type u_1} {p : αBool} {l : List α} (h : ∀ (a : α), a l¬p a = true) :
@[simp]
theorem List.eraseP_eq_nil {α : Type u_1} {xs : List α} {p : αBool} :
List.eraseP p xs = [] xs = [] ∃ (x : α), p x = true xs = [x]
theorem List.eraseP_ne_nil {α : Type u_1} {xs : List α} {p : αBool} :
List.eraseP p xs [] xs [] ∀ (x : α), p x = truexs [x]
theorem List.exists_of_eraseP {α : Type u_1} {p : αBool} {l : List α} {a : α} :
a lp a = true∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁¬p b = true) p a = true l = l₁ ++ a :: l₂ List.eraseP p l = l₁ ++ l₂
theorem List.exists_or_eq_self_of_eraseP {α : Type u_1} (p : αBool) (l : List α) :
List.eraseP p l = l ∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁¬p b = true) p a = true l = l₁ ++ a :: l₂ List.eraseP p l = l₁ ++ l₂
@[simp]
theorem List.length_eraseP_of_mem :
∀ {α : Type u_1} {l : List α} {a : α} {p : αBool}, a lp a = true(List.eraseP p l).length = l.length - 1
theorem List.length_eraseP {α : Type u_1} {p : αBool} {l : List α} :
(List.eraseP p l).length = if l.any p = true then l.length - 1 else l.length
theorem List.eraseP_sublist {α : Type u_1} {p : αBool} (l : List α) :
(List.eraseP p l).Sublist l
theorem List.eraseP_subset {α : Type u_1} {p : αBool} (l : List α) :
theorem List.Sublist.eraseP :
∀ {α : Type u_1} {l₁ l₂ : List α} {p : αBool}, l₁.Sublist l₂(List.eraseP p l₁).Sublist (List.eraseP p l₂)
theorem List.length_eraseP_le {α : Type u_1} {p : αBool} (l : List α) :
(List.eraseP p l).length l.length
theorem List.le_length_eraseP {α : Type u_1} {p : αBool} (l : List α) :
l.length - 1 (List.eraseP p l).length
theorem List.mem_of_mem_eraseP {α : Type u_1} {p : αBool} {a : α} {l : List α} :
a List.eraseP p la l
@[simp]
theorem List.mem_eraseP_of_neg {α : Type u_1} {p : αBool} {a : α} {l : List α} (pa : ¬p a = true) :
@[simp]
theorem List.eraseP_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
List.eraseP p l = l ∀ (a : α), a l¬p a = true
theorem List.eraseP_map {β : Type u_1} {α : Type u_2} {p : αBool} (f : βα) (l : List β) :
theorem List.eraseP_filterMap {α : Type u_1} {β : Type u_2} {p : βBool} (f : αOption β) (l : List α) :
List.eraseP p (List.filterMap f l) = List.filterMap f (List.eraseP (fun (x : α) => match f x with | some y => p y | none => false) l)
theorem List.eraseP_filter {α : Type u_1} {p : αBool} (f : αBool) (l : List α) :
List.eraseP p (List.filter f l) = List.filter f (List.eraseP (fun (x : α) => p x && f x) l)
theorem List.eraseP_append_left {α : Type u_1} {p : αBool} {a : α} (pa : p a = true) {l₁ : List α} (l₂ : List α) :
a l₁List.eraseP p (l₁ ++ l₂) = List.eraseP p l₁ ++ l₂
theorem List.eraseP_append_right {α : Type u_1} {p : αBool} {l₁ : List α} (l₂ : List α) :
(∀ (b : α), b l₁¬p b = true)List.eraseP p (l₁ ++ l₂) = l₁ ++ List.eraseP p l₂
theorem List.eraseP_append {α : Type u_1} {p : αBool} (l₁ : List α) (l₂ : List α) :
List.eraseP p (l₁ ++ l₂) = if l₁.any p = true then List.eraseP p l₁ ++ l₂ else l₁ ++ List.eraseP p l₂
theorem List.eraseP_replicate {α : Type u_1} (n : Nat) (a : α) (p : αBool) :
List.eraseP p (List.replicate n a) = if p a = true then List.replicate (n - 1) a else List.replicate n a
theorem List.IsPrefix.eraseP :
∀ {α : Type u_1} {l₁ l₂ : List α} {p : αBool}, l₁ <+: l₂List.eraseP p l₁ <+: List.eraseP p l₂
theorem List.eraseP_eq_iff {α : Type u_1} {l' : List α} {p : αBool} {l : List α} :
List.eraseP p l = l' (∀ (a : α), a l¬p a = true) l = l' ∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁¬p b = true) p a = true l = l₁ ++ a :: l₂ l' = l₁ ++ l₂
@[simp]
theorem List.eraseP_replicate_of_pos {α : Type u_1} {p : αBool} {n : Nat} {a : α} (h : p a = true) :
@[simp]
theorem List.eraseP_replicate_of_neg {α : Type u_1} {p : αBool} {n : Nat} {a : α} (h : ¬p a = true) :
theorem List.Pairwise.eraseP :
∀ {α : Type u_1} {p : ααProp} {l : List α} (q : αBool), List.Pairwise p lList.Pairwise p (List.eraseP q l)
theorem List.Nodup.eraseP :
∀ {α : Type u_1} {l : List α} (p : αBool), l.Nodup(List.eraseP p l).Nodup
theorem List.eraseP_comm {α : Type u_1} {p : αBool} {q : αBool} {l : List α} (h : ∀ (a : α), a l¬p a = true ¬q a = true) :
theorem List.head_eraseP_mem {α : Type u_1} (xs : List α) (p : αBool) (h : List.eraseP p xs []) :
(List.eraseP p xs).head h xs
theorem List.getLast_eraseP_mem {α : Type u_1} (xs : List α) (p : αBool) (h : List.eraseP p xs []) :
(List.eraseP p xs).getLast h xs

erase #

@[simp]
theorem List.erase_cons_head {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
(a :: l).erase a = l
@[simp]
theorem List.erase_cons_tail {α : Type u_1} [BEq α] {a : α} {b : α} {l : List α} (h : ¬(b == a) = true) :
(b :: l).erase a = b :: l.erase a
theorem List.erase_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
¬a ll.erase a = l
theorem List.erase_eq_eraseP' {α : Type u_1} [BEq α] (a : α) (l : List α) :
l.erase a = List.eraseP (fun (x : α) => x == a) l
theorem List.erase_eq_eraseP {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
l.erase a = List.eraseP (fun (x : α) => a == x) l
@[simp]
theorem List.erase_eq_nil {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {a : α} :
xs.erase a = [] xs = [] xs = [a]
theorem List.erase_ne_nil {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {a : α} :
xs.erase a [] xs [] xs [a]
theorem List.exists_erase_eq {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a l) :
∃ (l₁ : List α), ∃ (l₂ : List α), ¬a l₁ l = l₁ ++ a :: l₂ l.erase a = l₁ ++ l₂
@[simp]
theorem List.length_erase_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a l) :
(l.erase a).length = l.length - 1
theorem List.length_erase {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
(l.erase a).length = if a l then l.length - 1 else l.length
theorem List.erase_sublist {α : Type u_1} [BEq α] (a : α) (l : List α) :
(l.erase a).Sublist l
theorem List.erase_subset {α : Type u_1} [BEq α] (a : α) (l : List α) :
l.erase a l
theorem List.Sublist.erase {α : Type u_1} [BEq α] (a : α) {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) :
(l₁.erase a).Sublist (l₂.erase a)
theorem List.IsPrefix.erase {α : Type u_1} [BEq α] (a : α) {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) :
l₁.erase a <+: l₂.erase a
theorem List.length_erase_le {α : Type u_1} [BEq α] (a : α) (l : List α) :
(l.erase a).length l.length
theorem List.le_length_erase {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
l.length - 1 (l.erase a).length
theorem List.mem_of_mem_erase {α : Type u_1} [BEq α] {a : α} {b : α} {l : List α} (h : a l.erase b) :
a l
@[simp]
theorem List.mem_erase_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} (ab : a b) :
a l.erase b a l
@[simp]
theorem List.erase_eq_self_iff {α : Type u_1} [BEq α] {a : α} [LawfulBEq α] {l : List α} :
l.erase a = l ¬a l
theorem List.erase_filter {α : Type u_1} [BEq α] {a : α} [LawfulBEq α] (f : αBool) (l : List α) :
(List.filter f l).erase a = List.filter f (l.erase a)
theorem List.erase_append_left {α : Type u_1} [BEq α] {a : α} [LawfulBEq α] {l₁ : List α} (l₂ : List α) (h : a l₁) :
(l₁ ++ l₂).erase a = l₁.erase a ++ l₂
theorem List.erase_append_right {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : ¬a l₁) :
(l₁ ++ l₂).erase a = l₁ ++ l₂.erase a
theorem List.erase_append {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} {l₂ : List α} :
(l₁ ++ l₂).erase a = if a l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a
theorem List.erase_replicate {α : Type u_1} [BEq α] [LawfulBEq α] (n : Nat) (a : α) (b : α) :
(List.replicate n a).erase b = if (b == a) = true then List.replicate (n - 1) a else List.replicate n a
theorem List.erase_comm {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (b : α) (l : List α) :
(l.erase a).erase b = (l.erase b).erase a
theorem List.erase_eq_iff {α : Type u_1} [BEq α] {l' : List α} [LawfulBEq α] {a : α} {l : List α} :
l.erase a = l' ¬a l l = l' ∃ (l₁ : List α), ∃ (l₂ : List α), ¬a l₁ l = l₁ ++ a :: l₂ l' = l₁ ++ l₂
@[simp]
theorem List.erase_replicate_self {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a : α} :
(List.replicate n a).erase a = List.replicate (n - 1) a
@[simp]
theorem List.erase_replicate_ne {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a : α} {b : α} (h : (!b == a) = true) :
(List.replicate n a).erase b = List.replicate n a
theorem List.Pairwise.erase {α : Type u_1} [BEq α] {p : ααProp} [LawfulBEq α] {l : List α} (a : α) :
List.Pairwise p lList.Pairwise p (l.erase a)
theorem List.Nodup.erase_eq_filter {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} (d : l.Nodup) (a : α) :
l.erase a = List.filter (fun (x : α) => x != a) l
theorem List.Nodup.mem_erase_iff {α : Type u_1} [BEq α] {l : List α} {b : α} [LawfulBEq α] {a : α} (d : l.Nodup) :
a l.erase b a b a l
theorem List.Nodup.not_mem_erase {α : Type u_1} [BEq α] {l : List α} [LawfulBEq α] {a : α} (h : l.Nodup) :
¬a l.erase a
theorem List.Nodup.erase {α : Type u_1} [BEq α] {l : List α} [LawfulBEq α] (a : α) :
l.Nodup(l.erase a).Nodup
theorem List.head_erase_mem {α : Type u_1} [BEq α] (xs : List α) (a : α) (h : xs.erase a []) :
(xs.erase a).head h xs
theorem List.getLast_erase_mem {α : Type u_1} [BEq α] (xs : List α) (a : α) (h : xs.erase a []) :
(xs.erase a).getLast h xs

eraseIdx #

theorem List.length_eraseIdx {α : Type u_1} (l : List α) (i : Nat) :
(l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length
theorem List.length_eraseIdx_of_lt {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) :
(l.eraseIdx i).length = l.length - 1
@[simp]
theorem List.eraseIdx_zero {α : Type u_1} (l : List α) :
l.eraseIdx 0 = l.tail
theorem List.eraseIdx_eq_take_drop_succ {α : Type u_1} (l : List α) (i : Nat) :
l.eraseIdx i = List.take i l ++ List.drop (i + 1) l
@[simp]
theorem List.eraseIdx_eq_nil {α : Type u_1} {l : List α} {i : Nat} :
l.eraseIdx i = [] l = [] l.length = 1 i = 0
theorem List.eraseIdx_ne_nil {α : Type u_1} {l : List α} {i : Nat} :
l.eraseIdx i [] 2 l.length l.length = 1 i 0
theorem List.eraseIdx_sublist {α : Type u_1} (l : List α) (k : Nat) :
(l.eraseIdx k).Sublist l
theorem List.mem_of_mem_eraseIdx {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : a l.eraseIdx i) :
a l
theorem List.eraseIdx_subset {α : Type u_1} (l : List α) (k : Nat) :
l.eraseIdx k l
@[simp]
theorem List.eraseIdx_eq_self {α : Type u_1} {l : List α} {k : Nat} :
l.eraseIdx k = l l.length k
theorem List.eraseIdx_of_length_le {α : Type u_1} {l : List α} {k : Nat} (h : l.length k) :
l.eraseIdx k = l
theorem List.length_eraseIdx_le {α : Type u_1} (l : List α) (i : Nat) :
(l.eraseIdx i).length l.length
theorem List.le_length_eraseIdx {α : Type u_1} (l : List α) (i : Nat) :
l.length - 1 (l.eraseIdx i).length
theorem List.eraseIdx_append_of_lt_length {α : Type u_1} {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_1} {l : List α} {k : Nat} (hk : l.length k) (l' : List α) :
(l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)
theorem List.eraseIdx_replicate {α : Type u_1} {n : Nat} {a : α} {k : Nat} :
(List.replicate n a).eraseIdx k = if k < n then List.replicate (n - 1) a else List.replicate n a
theorem List.Pairwise.eraseIdx {α : Type u_1} {p : ααProp} {l : List α} (k : Nat) :
List.Pairwise p lList.Pairwise p (l.eraseIdx k)
theorem List.Nodup.eraseIdx {α : Type u_1} {l : List α} (k : Nat) :
l.Nodup(l.eraseIdx k).Nodup
theorem List.IsPrefix.eraseIdx {α : Type u_1} {l : List α} {l' : List α} (h : l <+: l') (k : Nat) :
l.eraseIdx k <+: l'.eraseIdx k