countP_cons_of_neg — Mathlib

English

If p a is false, then adding a to the front of s does not change the count: countP p (a ::ₘ s) = countP p s.

Русский

Если p(a) ложно, добавление a в начало s не меняет количество: countP p (a ::ₘ s) = countP p s.

LaTeX

$$$\neg p(a) \Rightarrow \operatorname{countP}(p, (a ::ₘ s)) = \operatorname{countP}(p, s)$$$

Lean4

@[simp]
theorem countP_cons_of_neg {a : α} (s) : ¬p a → countP p (a ::ₘ s) = countP p s :=
  Quot.inductionOn s <| by simpa using fun _ => List.countP_cons_of_neg (p := (p ·))

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