ennrealToMeasure_toENNRealVectorMeasure

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]

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