length_eraseP_add_one — Mathlib

English

If there exists an element a in l with p(a) true, then removing the first such element reduces the length by exactly 1.

Русский

Если в списке l существует элемент a с p(a)=true, то удаление первого такого элемента уменьшает длину на единицу.

LaTeX

$$$ \\exists a \\in l\\ (p\\,a = \\text{true}) \\Rightarrow |l\\setminus_p\\,l| = |l| - 1 $$$

Lean4

theorem length_eraseP_add_one {l : List α} {a} (al : a ∈ l) (pa : p a) : (l.eraseP p).length + 1 = l.length := by grind

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