restrict_restrict₀' — Mathlib

English

If t is null-measurable for μ, then restricting by t commutes with restricting by s: (μ|_t)|_s = μ|_{s∩t}.

Русский

Если t нулезмеримо относительно μ, то ограничение по t и затем по s равно ограничению по s∩t.

LaTeX

$$$ (\mu \restriction t) \restriction s = \mu \restriction (s \cap t) $ when $NullMeasurableSet t \mu$$$

Lean4

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

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