English
There is a natural inverse correspondence between ordinary measures on α and vector measures on α with ENNReal values, given by ennrealToMeasure and its inverse toENNRealVectorMeasure. Concretely, applying ennrealToMeasure to toENNRealVectorMeasure μ recovers μ for any measure μ.
Русский
Существует естественное обратное соответствие между мерами на α и векторными мерами на α со значениями в ENNReal, заданное функциями ennrealToMeasure и её обратной. Конкретно: ennrealToMeasure(toENNRealVectorMeasure(μ)) = μ для любой меры μ.
LaTeX
$$$$ \\operatorname{ennrealToMeasure}(\\operatorname{toENNRealVectorMeasure}(\\nu)) = \\nu $$$$
Lean4
@[simp]
theorem ennrealToMeasure_toENNRealVectorMeasure (μ : Measure α) : ennrealToMeasure (toENNRealVectorMeasure μ) = μ :=
Measure.ext fun s hs => by rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]