count_univ — Mathlib

English

The counting measure of the whole space equals the cardinality of the space, viewed in ENNReal.

Русский

Число счётной меры над всевозможным пространством равно кардинальности пространства, приведённой к ENNReal.

LaTeX

$$$count(\text{univ}) = \text{ENNat.card}(\alpha)$$$

Lean4

@[simp]
theorem count_univ : count (univ : Set α) = ENat.card α := by simp [count_apply .univ, encard_univ]

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