strictMono_of_hasDerivAt_pos — Mathlib

English

If a function f: R → R has a derivative that is strictly positive at every point, then f is strictly increasing on R.

Русский

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

LaTeX

$$$\forall x \in \mathbb{R},\; \exists f'(x) > 0 \;\Rightarrow\; f \text{ strictly increasing on } \mathbb{R}. $$$

Lean4

/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is strictly positive, then
`f` is a strictly monotone function. -/
theorem strictMono_of_hasDerivAt_pos {f f' : ℝ → ℝ} (hf : ∀ x, HasDerivAt f (f' x) x) (hf' : ∀ x, 0 < f' x) :
    StrictMono f :=
  strictMono_of_deriv_pos fun x ↦ by rw [(hf _).deriv]; exact hf' _

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