countP — Mathlib

English

countP p s counts the number of elements of s that satisfy p.

Русский

countP p s подсчитывает число элементов s, удовлетворяющих p.

LaTeX

$$$\mathrm{countP}\,p\,s = \text{Nat characteristic count of elements x with } p x$$$

Lean4

/-- `countP p s` counts the number of elements of `s` (with multiplicity) that
  satisfy `p`. -/
def countP (s : Multiset α) : ℕ :=
  Quot.liftOn s (List.countP p) fun _l₁ _l₂ => Perm.countP_eq (p ·)

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