nullMeasurableSet_lt — Mathlib

English

If f,g are AEMeasurable with respect to μ, then {a | f(a) < g(a)} is null‑measurable.

Русский

Если f,g — AEMeasurable по μ, то множество {a | f(a) < g(a)} нулево измеримо.

LaTeX

$$$\text{NullMeasurableSet}\{a\mid f(a)

Lean4

theorem nullMeasurableSet_lt [SecondCountableTopology α] {μ : Measure δ} {f g : δ → α} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) : NullMeasurableSet {a | f a < g a} μ :=
  (hf.prodMk hg).nullMeasurable measurableSet_lt'

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