length_erase_add_one — Mathlib

English

Removing a single element a from l decreases the length by 1, provided a is in l and equality is decidable.

Русский

Удаление одного элемента a из списка l уменьшает длину на единицу, если a принадлежит l и существует равенство.

LaTeX

$$$ a \\in l \\Rightarrow |l\\setminus a| + 1 = |l| $$$

Lean4

theorem length_erase_add_one {a : α} {l : List α} (h : a ∈ l) : (l.erase a).length + 1 = l.length := by
  rw [erase_eq_eraseP, length_eraseP_add_one h (decide_eq_true rfl)]

Похожие утверждения