restrict_mono' — Mathlib

English

If μ ≤ ν as measures, then μ|s ≤ ν|s for any set s.

Русский

Если μ ≤ ν как меры, то μ|s ≤ ν|s для любого множества s.

LaTeX

$$$\mu \le \nu \Rightarrow \mu|s ≤ ν|s.$$$

Lean4

/-- Restriction of a measure to a subset is monotone both in set and in measure. -/
theorem restrict_mono' {_m0 : MeasurableSpace α} ⦃s s' : Set α⦄ ⦃μ ν : Measure α⦄ (hs : s ≤ᵐ[μ] s') (hμν : μ ≤ ν) :
    μ.restrict s ≤ ν.restrict s' :=
  Measure.le_iff.2 fun t ht =>
    calc
      μ.restrict s t = μ (t ∩ s) := restrict_apply ht
      _ ≤ μ (t ∩ s') := (measure_mono_ae <| hs.mono fun _x hx ⟨hxt, hxs⟩ => ⟨hxt, hx hxs⟩)
      _ ≤ ν (t ∩ s') := (le_iff'.1 hμν (t ∩ s'))
      _ = ν.restrict s' t := (restrict_apply ht).symm

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