restrict_apply_superset — Mathlib

English

If S ⊆ T, then restricting to S and evaluating on T equals the mass of S: (μ restricted to S)(T) = μ(S).

Русский

Если S ⊆ T, то μ|_S(T) = μ(S).

LaTeX

$$$ (\mu \restriction S)(T) = \mu(S) \quad \text{iff} \quad S \subseteq T $$$

Lean4

theorem restrict_apply_superset (h : s ⊆ t) : μ.restrict s t = μ s :=
  ((measure_mono (subset_univ _)).trans_eq <| restrict_apply_univ _).antisymm
    ((restrict_apply_self μ s).symm.trans_le <| measure_mono h)

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