deriv_nonneg — Mathlib

English

If g is monotone, then its derivative exists everywhere nonnegative: deriv g x ≥ 0.

Русский

Если функция монотонна, то её производная существует и неотрицательна в любой точке: deriv g x ≥ 0.

LaTeX

$$(Monotone g) \\rightarrow 0 \\le deriv g x$$

Lean4

/-- The derivative of a monotone function is nonnegative. -/
theorem deriv_nonneg (hg : Monotone g) : 0 ≤ deriv g x :=
  by
  rw [← derivWithin_univ]
  exact (hg.monotoneOn univ).derivWithin_nonneg

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