countP' — Mathlib

English

The predicate-counting function countP' lifts to FreeMonoid α: for any l ∈ FreeMonoid α, countP' p l counts how many letters in l satisfy p.

Русский

Функция подсчета количества по предикату p, применяемая к элементу FreeMonoid α, подсчитывает, сколькими элементами списка, составляющего элемент, удовлетворяется p.

LaTeX

$$$\\operatorname{countP}'(p, l) = \\#\\{ x \\in l.\\mathrm{toList} \\,|\\, p(x) \\}$$$

Lean4

/-- `List.countP` lifted to free monoids -/
@[to_additive /-- `List.countP` lifted to free additive monoids -/
    ]
def countP' (l : FreeMonoid α) : ℕ :=
  l.toList.countP p

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