restrict_restrict₀ — Mathlib

English

Restricting by t and then by s, under a suitable null-measurability condition, is the same as restricting by s ∩ t.

Русский

Последовательное ограничение по t, затем по s равно ограничению по s ∩ t при условии нулевой меры.

LaTeX

$$$ (\mu \ restriction t).restriction s = \mu.restrict (s \cap t) $ under null-measurability conditions$$

Lean4

theorem restrict_restrict₀ (hs : NullMeasurableSet s (μ.restrict t)) : (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=
  ext fun u hu => by simp only [Set.inter_assoc, restrict_apply hu, restrict_apply₀ (hu.nullMeasurableSet.inter hs)]

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