measurable_encard — Mathlib

English

For countable α, the encard map from sets to extended naturals is measurable.

Русский

Для счетного множества α отображение encard: Set α → ℕ∞ измеримо.

LaTeX

$$$\\mathrm{Measurable}(\\mathrm{Set.encard} : \\mathrm{Set} \\alpha \\to \\mathbb{N}_\\infty)$$$

Lean4

@[measurability]
theorem measurable_encard : Measurable (Set.encard : Set α → ℕ∞) :=
  ENat.measurable_iff.2 fun _n ↦
    Countable.measurableSet <| Countable.setOf_finite.mono fun _s hs ↦ finite_of_encard_eq_coe hs

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