English
If a function f: R → R is differentiable everywhere and its derivative is positive at every point, then f is strictly increasing on R.
Русский
Если функция f: R → R дифференцируема на всей прямой и её производная положительна в каждой точке, то f строго возрастает на всей R.
LaTeX
$$$\text{If } f: \mathbb{R} \to \mathbb{R} \text{ is differentiable and } 0 < f'(x) \text{ for all } x \in \mathbb{R}, \text{ then } f \text{ is strictly increasing on } \mathbb{R}. $$$
Lean4
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is positive, then
`f` is a strictly monotone function.
Note that we don't require differentiability explicitly as it already implied by the derivative
being strictly positive. -/
theorem strictMono_of_deriv_pos {f : ℝ → ℝ} (hf' : ∀ x, 0 < deriv f x) : StrictMono f :=
strictMonoOn_univ.1 <|
strictMonoOn_of_deriv_pos convex_univ
(fun z _ => (differentiableAt_of_deriv_ne_zero (hf' z).ne').differentiableWithinAt.continuousWithinAt) fun x _ =>
hf' x
