ae_eq_trim_of_stronglyMeasurable — Mathlib

English

If f and g are strongly measurable and f equals g almost everywhere with respect to μ, then they are equal almost everywhere with respect to the trimmed measure μ.trim hm.

Русский

Если f и g сильно измеримы и равноcь f и g почти всюду по μ, то они равны почти всюду по обрезанной мере μ.trim hm.

LaTeX

$$$ f =_{\mathrm{ae},\mu} g \Rightarrow f =_{\mathrm{ae},\mu_{\mathrm{trim}(hm)}} g $$$

Lean4

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

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