integral_mono — Mathlib

English

If f ≤ g almost everywhere and both are integrable, then the integral of f is at most the integral of g.

Русский

Если f ≤ g почти повсюду и оба интегрируемы, то интеграл f не превышает интеграл g.

LaTeX

$$$$ \\int f \\leq \\int g \\quad\\text{whenever } f \\leq g \\text{ a.e. and both integrable}. $$$$

Lean4

theorem integral_mono {f g : α →ₛ F} (h : f ≤ᵐ[μ] g) (hf : Integrable f μ) (hg : Integrable g μ) :
    f.integral μ ≤ g.integral μ := by
  rw [← sub_nonneg, ← integral_sub hg hf]
  rw [← sub_nonneg_ae] at h
  exact integral_nonneg h

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