English
The extended nonnegative reals ENNReal carry a MeasurablePow structure, i.e., the power operation on ENNReal is measurable.
Русский
У ENNReal имеется структура измеримого возведения в степень, т.е. возведение в степень на ENNReal измеримо.
LaTeX
$$$\\text{ENNReal.HasMeasurablePow}$$$
Lean4
instance hasMeasurablePow : MeasurablePow ℝ≥0∞ ℝ :=
by
refine ⟨ENNReal.measurable_of_measurable_nnreal_prod ?_ ?_⟩
· simp_rw [ENNReal.coe_rpow_def]
refine Measurable.ite ?_ measurable_const (measurable_fst.pow measurable_snd).coe_nnreal_ennreal
exact MeasurableSet.inter (measurable_fst (measurableSet_singleton 0)) (measurable_snd measurableSet_Iio)
· simp_rw [ENNReal.top_rpow_def]
refine Measurable.ite measurableSet_Ioi measurable_const ?_
exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const
