ennrealEquivSum — Mathlib

English

There exists a MeasurableEquiv between ENNReal and the sum NNReal ⊕ Unit, i.e., ENNReal is measurably isomorphic to NNReal ⊕ Unit.

Русский

Существует измеримая эквивалентность между ENNReal и суммой NNReal ⊕ Unit, т.е. ENNReal измеримо эквивалентно NNReal ⊕ Unit.

LaTeX

$$$\text{ENNReal} \cong^m (\mathbb{R}_{\ge 0} \oplus \mathrm{Unit})$$$

Lean4

/-- `ℝ≥0∞` is `MeasurableEquiv` to `ℝ≥0 ⊕ Unit`. -/
def ennrealEquivSum : ℝ≥0∞ ≃ᵐ ℝ≥0 ⊕ Unit :=
  {
    Equiv.optionEquivSumPUnit
      ℝ≥0 with
    measurable_toFun := measurable_of_measurable_nnreal measurable_inl
    measurable_invFun := measurable_fun_sum measurable_coe_nnreal_ennreal (@measurable_const ℝ≥0∞ Unit _ _ ∞) }

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