le_restrict_apply — Mathlib

English

Let s and t be sets in a measure space. Then the mass of t ∩ s is no larger than the mass of t under the restricted measure to s; equivalently, μ(t ∩ s) ≤ (μ restricted to s)(t).

Русский

Пусть S и T — множества в мереобразном пространстве. Тогда масса m(T ∩ S) не превосходит массы m, ограниченной до S, на множестве T; то есть μ(T ∩ S) ≤ (μ restriction to S)(T).

LaTeX

$$$\mu(t \cap s) \le (\mu \restriction s)(t)$$$

Lean4

theorem le_restrict_apply (s t : Set α) : μ (t ∩ s) ≤ μ.restrict s t :=
  calc
    μ (t ∩ s) = μ.restrict s (t ∩ s) := (restrict_eq_self μ inter_subset_right).symm
    _ ≤ μ.restrict s t := measure_mono inter_subset_left

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