English
There is a canonical equivalence between vector measures with ENNReal values and ordinary measures on α, implemented by ennrealToMeasure and toENNRealVectorMeasure. These maps are inverse to each other.
Русский
Существует каноническое эквивалентное соответствие между векторными мерами с значениями ENNReal и обычными мерами на α, реализованное через ennrealToMeasure и toENNRealVectorMeasure. Эти отображения являются взаимно обратными.
LaTeX
$$$$ \\text{ennrealToMeasure} \\mathrel{:} \\text{VectorMeasure}(\\alpha, \\mathbb{R}_{\\ge 0,\\infty}) \\to \\text{Measure}(\\alpha), \\quad \\text{toENNRealVectorMeasure} \\mathrel{:} \\text{Measure}(\\alpha) \\to \\text{VectorMeasure}(\\alpha, \\mathbb{R}_{\\ge 0,\\infty}) $$\n\\text{ and }\\n\\text{ennrealToMeasure} \\circ \\text{toENNRealVectorMeasure} = \\mathrm{id},\\quad \\text{toENNRealVectorMeasure} \\circ \\text{ennrealToMeasure} = \\mathrm{id}. $$$$
Lean4
/-- The equiv between `VectorMeasure α ℝ≥0∞` and `Measure α` formed by
`MeasureTheory.VectorMeasure.ennrealToMeasure` and
`MeasureTheory.Measure.toENNRealVectorMeasure`. -/
@[simps]
def equivMeasure [MeasurableSpace α] : VectorMeasure α ℝ≥0∞ ≃ Measure α
where
toFun := ennrealToMeasure
invFun := toENNRealVectorMeasure
left_inv := toENNRealVectorMeasure_ennrealToMeasure
right_inv := ennrealToMeasure_toENNRealVectorMeasure
