nonneg_of_monotone — Mathlib

English

If HasDerivAt g g' x holds and g is monotone, then the derivative g' is nonnegative: 0 ≤ g'.

Русский

Если существует производная HasDerivAt g g' x и функция g монотонна, то производная неотрицательна: 0 ≤ g'.

LaTeX

$$(HasDerivAt(g,g',x)) \\rightarrow (Monotone(g)) \\rightarrow 0 \\le g'$$

Lean4

/-- If a monotone function has a derivative, then this derivative is nonnegative. -/
theorem nonneg_of_monotone (hd : HasDerivAt g g' x) (hg : Monotone g) : 0 ≤ g' :=
  by
  rw [← hasDerivWithinAt_univ] at hd
  apply hd.nonneg_of_monotoneOn _ (hg.monotoneOn _)
  exact PerfectSpace.univ_preperfect _ (mem_univ _)

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