count_eq_card_fintype — Mathlib

English

For any predicate p, count p n equals the cardinality of the subtype { k : ℕ // k < n ∧ p k }.

Русский

Для любого предиката p count p n равно кардинальности подтипа {k : ℕ // k < n ∧ p k}.

LaTeX

$$$$\operatorname{count}(p,n) = \operatorname{Fintype.card} \{ k : \mathbb{N} \mid k < n \wedge p(k) \}.$$$$

Lean4

/-- `count p n` can be expressed as the cardinality of `{k // k < n ∧ p k}`. -/
theorem count_eq_card_fintype (n : ℕ) : count p n = Fintype.card { k : ℕ // k < n ∧ p k } :=
  by
  rw [count_eq_card_filter_range, Fintype.card_of_subtype]
  simp

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