restrict_apply₀' — Mathlib

English

Restriction commutes with toOuterMeasure: (μ|s).toOuterMeasure = OuterMeasure.restrict s μ.toOuterMeasure.

Русский

Ограничение и переход к внешней мере коммутируют: (μ|s).toOuterMeasure = OuterMeasure.restrict s μ.toOuterMeasure.

LaTeX

$$$(\mu|s).toOuterMeasure = OuterMeasure.restrict(s,\mu.toOuterMeasure).$$$

Lean4

theorem restrict_apply₀' (hs : NullMeasurableSet s μ) : μ.restrict s t = μ (t ∩ s) := by
  rw [← restrict_congr_set hs.toMeasurable_ae_eq, restrict_apply' (measurableSet_toMeasurable _ _),
    measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)]

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