integral_nonneg — Mathlib

English

If f ≤ g almost everywhere on Ioc(a,b) and both are interval-integrable on [a,b], then ∫_a^b f ≤ ∫_a^b g.

Русский

Если f ≤ g почти всюду на Ioc(a,b) и оба интегрируемы на [a,b], то интеграл f ≤ интеграл g.

LaTeX

$$$f \\le^a_{\\mu.restrict(Ioc(a,b))} g \\Rightarrow ∫_a^b f ≤ ∫_a^b g$$$

Lean4

theorem integral_nonneg (hab : a ≤ b) (hf : ∀ u, u ∈ Icc a b → 0 ≤ f u) : 0 ≤ ∫ u in a..b, f u ∂μ :=
  integral_nonneg_of_ae_restrict hab <| (ae_restrict_iff' measurableSet_Icc).mpr <| ae_of_all μ hf

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