integral_nonneg_of_forall — Mathlib

English

If f is nonnegative on all arguments (∀u, f(u) ≥ 0) and f is interval-integrable on [a,b], then ∫_a^b f ≥ 0.

Русский

Если f неотрицательна для всех аргументов и интегрируема на [a,b], тогда интеграл неотрицателен.

LaTeX

$$$hab: a \\le b,\\ hf: \\forall u, f(u) \\ge 0 \\Rightarrow 0 ≤ ∫_a^b f$$$

Lean4

theorem integral_nonneg_of_forall (hab : a ≤ b) (hf : ∀ u, 0 ≤ f u) : 0 ≤ ∫ u in a..b, f u ∂μ :=
  integral_nonneg_of_ae hab <| Eventually.of_forall hf

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