restrict_restrict_of_subset — Mathlib

English

If S ⊆ T, then restricting to T then to S equals restricting directly to S: (μ|_T)|_S = μ|_S.

Русский

Если S ⊆ T, то ограничение до T, затем до S равно ограничению до S: (μ|_T)|_S = μ|_S.

LaTeX

$$$ (\mu \restriction T) \restriction S = \mu \restriction S $ whenever $S \subseteq T$$$

Lean4

theorem restrict_restrict_of_subset (h : s ⊆ t) : (μ.restrict t).restrict s = μ.restrict s :=
  by
  ext1 u hu
  rw [restrict_apply hu, restrict_apply hu, restrict_eq_self]
  exact inter_subset_right.trans h

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