ae_le_of_forall_setLIntegral_le_of_sigmaFinite

English

If measurable f,g: α→ℝ≥0∞ satisfy ∀ s measurable with finite μ(s), ∫⁻ f ≤ ∫⁻ g on s, then f ≤ a.e. g and g ≤ a.e. f; hence f=g a.e.

Русский

Если измеримые функции удовлетворяют неравенствам интегралов на каждом конечном множестве, то они равны почти повсюду.

LaTeX

$$$$ f =^{\mathrm{ae}}_{\mu} g $$$$

Lean4

theorem ae_le_of_forall_setLIntegral_le_of_sigmaFinite [SigmaFinite μ] {f g : α → ℝ≥0∞} (hf : Measurable f)
    (h : ∀ s, MeasurableSet s → μ s < ∞ → (∫⁻ x in s, f x ∂μ) ≤ ∫⁻ x in s, g x ∂μ) : f ≤ᵐ[μ] g :=
  ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hf.aemeasurable h

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