nullMeasurableSet_lt — Mathlib

English

If f and g are AEStronglyMeasurable, then the set {a | f(a) ≤ g(a)} is null-measurable.

Русский

Если f и g — AEStronglyMeasurable, множество {a | f(a) ≤ g(a)} нуль-измеримо.

LaTeX

$$$AEStronglyMeasurable(f, \mu) \land AEStronglyMeasurable(g, \mu) \Rightarrow NullMeasurableSet\{a \mid f(a) \le g(a)\}, \mu$$$

Lean4

theorem nullMeasurableSet_lt [Preorder β] [OrderClosedTopology β] [PseudoMetrizableSpace β] {f g : α → β}
    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : NullMeasurableSet {a | f a < g a} μ :=
  by
  apply (hf.stronglyMeasurable_mk.measurableSet_lt 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]

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