English
There is a natural inverse correspondence between vector measures on α taking values in ENNReal and ordinary measures on α. Concretely, applying ennrealToMeasure to a vector measure and then taking its vector measure back via toENNRealVectorMeasure yields the original vector measure.
Русский
Существует естественное обратное соответствие между векторными мерами на пространствах α со значениями в ENNReal и обычными мерами на α. Конкретно: применение ennrealToMeasure к векторной мере, а затем возврат через toENNRealVectorMeasure даёт исходную векторную меру.
LaTeX
$$$\\operatorname{toENNRealVectorMeasure}(\\operatorname{ennrealToMeasure}(\\mu)) = \\mu$$$
Lean4
@[simp]
theorem _root_.MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure (μ : VectorMeasure α ℝ≥0∞) :
toENNRealVectorMeasure (ennrealToMeasure μ) = μ :=
ext fun s hs => by rw [toENNRealVectorMeasure_apply_measurable hs, ennrealToMeasure_apply hs]