toOuterMeasure_eq_inducedOuterMeasure

English

The outer measure equals the inducedOuterMeasure of the map s ↦ μ s.

Русский

Внешняя мера равна индуцированной внешней мере от отображения s ↦ μ s.

LaTeX

$$$\mu.toOuterMeasure = \operatorname{inducedOuterMeasure}(s \mapsto \mu s)\ MeasurableSet.empty \mu.empty$$$

Lean4

theorem toOuterMeasure_eq_inducedOuterMeasure :
    μ.toOuterMeasure = inducedOuterMeasure (fun s _ => μ s) MeasurableSet.empty μ.empty :=
  μ.trimmed.symm

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