toENNRealVectorMeasure_ennrealToMeasure

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]

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