instMeasurableMul₂ — Mathlib

English

There is a MeasurableMul₂ structure on ENNReal, i.e., multiplication of ENNReal in two arguments is measurable.

Русский

Существует структура MeasurableMul₂ на ENNReal: двухаргуменная умножение измеримо.

LaTeX

$$$\text{MeasurableMul₂ } \mathbb{R}_{\ge 0}^{\infty}$$$

Lean4

instance instMeasurableMul₂ : MeasurableMul₂ ℝ≥0∞ :=
  by
  refine ⟨measurable_of_measurable_nnreal_nnreal ?_ ?_ ?_⟩
  · simp only [← ENNReal.coe_mul, measurable_mul.coe_nnreal_ennreal]
  · simp only [ENNReal.top_mul', ENNReal.coe_eq_zero]
    exact measurable_const.piecewise (measurableSet_singleton _) measurable_const
  · simp only [ENNReal.mul_top', ENNReal.coe_eq_zero]
    exact measurable_const.piecewise (measurableSet_singleton _) measurable_const

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