ae_eq_trim_of_measurable — Mathlib

English

If hm is a refinement of σ-algebras and f,g are μ-measurable with respect to m, and f =ᵐ[μ] g, then f =ᵐ[μ.trim hm] g.

Русский

Если hm—развертка σ-алгебр, и f,g измеримы по μ относительно m и f =ᵐ[μ] g, то f =ᵐ[μ.trim hm] g.

LaTeX

$$$f =^\\mu g \\Rightarrow f =^\\mu_{\\mathrm{trim}(hm)} g$$$

Lean4

theorem ae_eq_trim_of_measurable {α E} {m m0 : MeasurableSpace α} {μ : Measure α} [MeasurableSpace E] [AddGroup E]
    [MeasurableSingletonClass E] [MeasurableSub₂ E] (hm : m ≤ m0) {f g : α → E} (hf : Measurable[m] f)
    (hg : Measurable[m] g) (hfg : f =ᵐ[μ] g) : f =ᵐ[μ.trim hm] g :=
  by
  rwa [Filter.EventuallyEq, ae_iff, trim_measurableSet_eq hm _]
  exact @MeasurableSet.compl α _ m (@measurableSet_eq_fun α m E _ _ _ _ _ _ hf hg)

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