restrict_mono — Mathlib

English

If s ⊆ t, then μ|s ≤ μ|t for any measure μ.

Русский

Если s ⊆ t, то для любой меры μ верно μ|s ≤ μ|t.

LaTeX

$$$s \subseteq t \Rightarrow \mu|s ≤ \mu|t.$$$

Lean4

/-- Restriction of a measure to a subset is monotone both in set and in measure. -/
@[mono, gcongr]
theorem restrict_mono {_m0 : MeasurableSpace α} ⦃s s' : Set α⦄ (hs : s ⊆ s') ⦃μ ν : Measure α⦄ (hμν : μ ≤ ν) :
    μ.restrict s ≤ ν.restrict s' :=
  restrict_mono' (ae_of_all _ hs) hμν

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