restrict_eq_self — Mathlib

English

For s ⊆ t, the restricted measure μ|t restricted to s equals μ|s, i.e., μ|t(s) = μ(s).

Русский

Для s ⊆ t ограниченная мера μ|t на s равна μ|s, то есть μ|t(s) = μ(s).

LaTeX

$$$s \subseteq t \Rightarrow (\mu|_{t})(s) = \mu(s).$$$

Lean4

theorem restrict_eq_self (h : s ⊆ t) : μ.restrict t s = μ s :=
  (le_iff'.1 restrict_le_self s).antisymm <|
    calc
      μ s ≤ μ (toMeasurable (μ.restrict t) s ∩ t) := measure_mono (subset_inter (subset_toMeasurable _ _) h)
      _ = μ.restrict t s := by rw [← restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]

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