count — Mathlib

English

For a predicate p on natural numbers, count p n denotes the number of integers k with 0 ≤ k < n and p(k).

Русский

Для предиката p на натуральных числе count p n обозначает количество чисел k, таких что 0 ≤ k < n и p(k).

LaTeX

$$$$\operatorname{count}(p,n) = \#\{ k \in \mathbb{N} \mid 0 \le k < n \text{ и } p(k) \}.$$$$

Lean4

/-- Count the number of naturals `k < n` satisfying `p k`. -/
def count (n : ℕ) : ℕ :=
  (List.range n).countP p

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