countP — Mathlib

English

For any x ∈ α, countP' p (of x) = 1 if p(x) holds, else 0.

Русский

Для единичного слова of(x) подсчет countP' равен 1, если p(x) истинно, иначе 0.

LaTeX

$$$\\operatorname{countP}'(p, \\mathrm{of}(x)) = \\begin{cases} 1, & p(x) \\\\ 0, & \\text{не } p(x) \\end{cases}$$$

Lean4

/-- `List.countP` as a bundled multiplicative monoid homomorphism. -/
def countP : FreeMonoid α →* Multiplicative ℕ
    where
  toFun := .ofAdd ∘ FreeMonoid.countP' p
  map_one' := by simp [countP'_one p]
  map_mul' x y := by simp [countP'_mul p]

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