monotone_of_deriv_nonneg — Mathlib

English

If f: R → R is differentiable and its derivative is nonnegative for all x, then f is monotone (nondecreasing) on R.

Русский

Если f: R → R дифференцируема и её производная неотрицательна на всей R, то f монотонна (неубывает) на R.

LaTeX

$$$\forall x,y \in \mathbb{R},\; x \le y \Rightarrow f(x) \le f(y)\quad\text{provided } \forall x, \; f'(x) \ge 0.$$$

Lean4

/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
`f` is a monotone function. -/
theorem monotone_of_deriv_nonneg {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf' : ∀ x, 0 ≤ deriv f x) : Monotone f :=
  monotoneOn_univ.1 <|
    monotoneOn_of_deriv_nonneg convex_univ hf.continuous.continuousOn hf.differentiableOn fun x _ => hf' x

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