restrict_toOuterMeasure_eq_toOuterMeasure_restrict

English

Restriction and the operation toOuterMeasure commute: the outer measure of the restricted measure equals the restriction of the outer measure.

Русский

Ограничение и переход к внешней мере совместимы: внешняя мера ограниченной меры равна ограничению внешней меры.

LaTeX

$$$(\mu\restriction s).toOuterMeasure = OuterMeasure.restrict s \mu.toOuterMeasure.$$$

Lean4

/-- This lemma shows that `restrict` and `toOuterMeasure` commute. Note that the LHS has a
restrict on measures and the RHS has a restrict on outer measures. -/
theorem restrict_toOuterMeasure_eq_toOuterMeasure_restrict (h : MeasurableSet s) :
    (μ.restrict s).toOuterMeasure = OuterMeasure.restrict s μ.toOuterMeasure := by
  simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk, toMeasure_toOuterMeasure,
    OuterMeasure.restrict_trim h, μ.trimmed]

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