countPAddMonoidHom — Mathlib

English

For a predicate p, the function countP p extends to an AddMonoidHom countPAddMonoidHom p: Multiset α →+ ℕ, with toFun(s) = countP p s and additivity/count properties given by countP.

Русский

Для предиката p отображение countP p распространяется до AddMonoidHom: Multiset α →+ ℕ, с toFun(s) = countP p s и аддитивностью.

LaTeX

$$$\text{countPAddMonoidHom } p: \mathrm{Multiset}(\alpha) \to^+ \mathbb{N},\quad\text{toFun}(s)=\operatorname{countP} p s.$$$

Lean4

/-- `countP p`, the number of elements of a multiset satisfying `p`, promoted to an
`AddMonoidHom`. -/
def countPAddMonoidHom : Multiset α →+ ℕ where
  toFun := countP p
  map_zero' := countP_zero _
  map_add' := countP_add _

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