restrict_restrict — Mathlib

English

Restricting by S then by T is the same as restricting by T then by S, provided S,T are measurable.

Русский

Ограничение по S и затем по T равно ограничению по T и затем по S при измеримости S и T.

LaTeX

$$$ (\mu \restriction T).restriction S = (\mu \restriction S).restriction T $ for MeasurableSet S$$

Lean4

@[simp]
theorem restrict_restrict (hs : MeasurableSet s) : (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=
  restrict_restrict₀ hs.nullMeasurableSet

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