restrict_comm — Mathlib

English

If S is measurable, restricting by T then by S equals restricting by S then by T, i.e., (μ|_T)|_S = (μ|_S)|_T.

Русский

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

LaTeX

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

Lean4

theorem restrict_comm (hs : MeasurableSet s) : (μ.restrict t).restrict s = (μ.restrict s).restrict t := by
  rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]

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