English
If you erase an element a from a list l, the count of p-values decreases by 1 exactly when a appears in l and p(a) is true; otherwise it decreases by 0.
Русский
Если удалить элемент a из списка l, число истин для p уменьшается на 1 тогда, когда a встречается в l и p(a)=true; иначе на 0.
LaTeX
$$$countP\\ p\\ (l\\ erase\\ a) = countP\\ p\\ l - \\text{if } a\\in l \\land p(a)=\\mathrm{true} \\text{ then } 1 \\text{ else } 0$$$
Lean4
theorem countP_erase (p : α → Bool) (l : List α) (a : α) :
countP p (l.erase a) = countP p l - if a ∈ l ∧ p a then 1 else 0 :=
by
rw [countP_eq_length_filter, countP_eq_length_filter, ← erase_filter, length_erase]
aesop
