count_eq_card_filter_range — Mathlib

English

The count of p up to n equals the cardinality of the set {x in range n | p x}.

Русский

Число элементов, удовлетворяющих p до n, равно кардинальности множества {x ∈ range(n) | p x}.

LaTeX

$$$$\operatorname{count}(p,n) = \#\{ x \in \mathrm{range}(n) \mid p(x) \}.$$$$

Lean4

theorem count_eq_card_filter_range (n : ℕ) : count p n = #({x ∈ range n | p x}) :=
  by
  rw [count, List.countP_eq_length_filter]
  rfl

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