nullMeasurableSet_le — Mathlib

English

If f,g: δ→α are AEMeasurable, then {a | f(a) ≤ g(a)} is null‑measurable.

Русский

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

LaTeX

$$$\text{NullMeasurableSet}\{a\mid f(a)\le g(a)\}\,\mu$$$

Lean4

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

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