ae_le_trim_of_stronglyMeasurable — Mathlib

English

If f ≤ᵐ g almost everywhere with respect to μ, then f ≤ᵐ g with respect to the trimmed measure μ.trim hm.

Русский

Если f ≤ᵐ g почти везде по μ, то f ≤ᵐ g по триммированной мере μ.trim hm.

LaTeX

$$$f \leq_{ae}^{\mu} g \Rightarrow f \leq_{ae}^{\mu^{\mathrm{trim}}} g$$$

Lean4

theorem ae_le_trim_of_stronglyMeasurable (hm : m ≤ m₀) (hf : StronglyMeasurable[m] f) (hg : StronglyMeasurable[m] g)
    (hfg : f ≤ᵐ[μ] g) : f ≤ᵐ[μ.trim hm] g :=
  by
  rwa [EventuallyLE, ae_iff, trim_measurableSet_eq hm]
  exact (hf.measurableSet_le hg).compl

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