English
If two functions f,g are measurable with respect to m, and f =ᵐ[μ] g, then they are equal μ-trim-measurably almost everywhere with respect to μ.trim hm for hm: m ≤ m0.
Русский
Если f,g измеримы по m и f =ᵐ[μ] g, то они равны μ-обрезке hn по отношению к μ.trim hm, где hm: m ≤ m0.
LaTeX
$$$f =^\\mu g \\Rightarrow f =^\\mu_{\\mathrm{trim}(hm)} g$$$
Lean4
theorem nullMeasurableSet_eq_fun {E} [MeasurableSpace E] [AddGroup E] [MeasurableSingletonClass E] [MeasurableSub₂ E]
{f g : α → E} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : NullMeasurableSet {x | f x = g x} μ :=
by
apply (measurableSet_eq_fun hf.measurable_mk hg.measurable_mk).nullMeasurableSet.congr
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx
change (hf.mk f x = hg.mk g x) = (f x = g x)
simp only [hfx, hgx]
