integral_mono — Mathlib

English

If f ≤ g on Ioo(a,b) then ∫_a^b f ≤ ∫_a^b g for suitable integrability conditions.

Русский

Если f ≤ g на Ioo(a,b), то интеграл f не превышает интеграл g, при надлежащей интегрируемости.

LaTeX

$$$\\forall f,g: f ≤ g on Ioo(a,b) \\Rightarrow ∫_a^b f ≤ ∫_a^b g$$$

Lean4

theorem integral_mono (h : f ≤ g) : (∫ u in a..b, f u ∂μ) ≤ ∫ u in a..b, g u ∂μ :=
  integral_mono_ae hab hf hg <| ae_of_all _ h

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