countP_of — Mathlib

English

For x ∈ α, countP p (of x) equals 1 if p(x) holds, else 0, interpreted in Multiplicative ℕ.

Русский

Для x ∈ α, countP p (of x) равно 1, если p(x) истинно, иначе 0, в Multiplicative ℕ.

LaTeX

$$$\\operatorname{countP}(p)(\\mathrm{of}(x)) = \\begin{cases} \\mathrm{Multiplicative}(1), & p(x) \\\\ \\mathrm{Multiplicative}(0), & \\neg p(x) \\end{cases}$$$

Lean4

theorem countP_of (x : α) : (of x).countP p = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0 :=
  by
  rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)]
  simp only [decide_eq_true_eq]

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