countP_cons — Mathlib

English

For any a and s, countP p (a ::ₘ s) = countP p s + if p a then 1 else 0.

Русский

Для любых a и s верно: countP p (a ::ₘ s) = countP p s + если p a, то 1, иначе 0.

LaTeX

$$$\operatorname{countP}(p, (a ::ₘ s)) = \operatorname{countP}(p, s) + \text{if } p(a) \text{ then } 1 \text{ else } 0$$$

Lean4

theorem countP_cons (b : α) (s) : countP p (b ::ₘ s) = countP p s + if p b then 1 else 0 :=
  Quot.inductionOn s <| by simp [List.countP_cons]

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