monotone_of_hasDerivAt_nonneg — Mathlib

English

If f is differentiable on R and its derivative is nonnegative (f'(x) ≥ 0) for every x, then f is monotone on R.

Русский

Если f дифференцируема на R и её производная неотрицательна в каждой точке, то f монотонна на R.

LaTeX

$$$\forall x,y \in \mathbb{R},\; x \le y \Rightarrow f(x) \le f(y)\quad\text{given } \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_hasDerivAt_nonneg {f f' : ℝ → ℝ} (hf : ∀ x, HasDerivAt f (f' x) x) (hf' : 0 ≤ f') : Monotone f :=
  monotone_of_deriv_nonneg (fun _ ↦ (hf _).differentiableAt) fun x ↦ by rw [(hf _).deriv]; exact hf' _

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