toOuterMeasure_trim_eq_trim_toOuterMeasure

English

For measures on a space with two comparable σ-algebras m ≤ m0, the outer measure of the trimmed measure equals the outer measure trim of μ: toOuterMeasure(μ.trim hm) = OuterMeasure.trim(μ.toOuterMeasure).

Русский

Для меры μ и двух согласованных σ-алгебр m ≤ m0 выполняется равенство внешней меры обрезанной меры и обрезанной внешней меры: toOuterMeasure(μ.trim hm) = OuterMeasure.trim(μ.toOuterMeasure).

LaTeX

$$$\\operatorname{toOuterMeasure}(\\mu_{\\mathrm{trim}(hm)}) = \\operatorname{OuterMeasure.trim}(\\mu^{\\mathrm{toOuterMeasure}}).$$$

Lean4

theorem toOuterMeasure_trim_eq_trim_toOuterMeasure (μ : Measure α) (hm : m ≤ m0) :
    @Measure.toOuterMeasure _ m (μ.trim hm) = @OuterMeasure.trim _ m μ.toOuterMeasure := by
  rw [Measure.trim, toMeasure_toOuterMeasure (ms := m)]

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