English
Let hm ≤ m ≤ m0. If f and g are AEStronglyMeasurable with respect to m, then hfm.mk f =ᵐ[μ.trim hm] hgm.mk g iff f =ᵐ[μ] g.
Русский
Пусть hm ≤ m ≤ m0. Если f и g являются AEStronglyMeasurable по отношению к m, то равенство почти повсюду после усечения мер μ.trim hm эквивалентно равенству почти повсюду по μ.
LaTeX
$$$\forall hm\, (hf, hg) : (AEStronglyMeasurable[m] f\mu)\times (AEStronglyMeasurable[m] g\mu) \Rightarrow \big( hfm.mk f =ᵐ[\mu.\text{trim } hm] hgm.mk g \Leftrightarrow f =ᵐ[\mu] g \big)$$$
Lean4
theorem ae_eq_trim_iff_of_aestronglyMeasurable {α β} [TopologicalSpace β] [MetrizableSpace β] {m m0 : MeasurableSpace α}
{μ : Measure α} {f g : α → β} (hm : m ≤ m0) (hfm : AEStronglyMeasurable[m] f μ)
(hgm : AEStronglyMeasurable[m] g μ) : hfm.mk f =ᵐ[μ.trim hm] hgm.mk g ↔ f =ᵐ[μ] g :=
(hfm.stronglyMeasurable_mk.ae_eq_trim_iff hm hgm.stronglyMeasurable_mk).trans
⟨fun h => hfm.ae_eq_mk.trans (h.trans hgm.ae_eq_mk.symm), fun h => hfm.ae_eq_mk.symm.trans (h.trans hgm.ae_eq_mk)⟩
