ae_eq_trim_iff — Mathlib

English

For strongly measurable f,g, equality almost everywhere with respect to the trimmed measure is equivalent to equality almost everywhere with respect to the original measure.

Русский

Для сильно измеримых функций f,g равенство почти всюду по обрезанной мере равно равенству почти всюду по исходной мере.

LaTeX

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

Lean4

theorem ae_eq_trim_iff (hm : m ≤ m₀) (hf : StronglyMeasurable[m] f) (hg : StronglyMeasurable[m] g) :
    f =ᵐ[μ.trim hm] g ↔ f =ᵐ[μ] g :=
  ⟨ae_eq_of_ae_eq_trim, ae_eq_trim_of_stronglyMeasurable hm hf hg⟩

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