nullMeasurableSet_eq_fun — Mathlib

English

If f is AEStronglyMeasurable, then the set where f is nonzero (mulSupport) is null-measurable.

Русский

Если f AEStronglyMeasurable, то mulSupport(f) является нуль-измеримой множеством.

LaTeX

$$$AEStronglyMeasurable(f, \mu) \Rightarrow NullMeasurableSet(Function.mulSupport(f), \mu)$$$

Lean4

theorem nullMeasurableSet_eq_fun {E} [TopologicalSpace E] [MetrizableSpace E] {f g : α → E}
    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : NullMeasurableSet {x | f x = g x} μ :=
  by
  apply (hf.stronglyMeasurable_mk.measurableSet_eq_fun hg.stronglyMeasurable_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]

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