strictAnti_of_deriv_neg — Mathlib

English

If a differentiable function has strictly negative derivative everywhere, then it is strictly decreasing on the real line.

Русский

Если производная строго положительна нигде, функция строго убывает на ℝ.

LaTeX

$$$\forall x

Lean4

/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is negative, then
`f` is a strictly antitone function.
Note that we don't require differentiability explicitly as it already implied by the derivative
being strictly negative. -/
theorem strictAnti_of_deriv_neg {f : ℝ → ℝ} (hf' : ∀ x, deriv f x < 0) : StrictAnti f :=
  strictAntiOn_univ.1 <|
    strictAntiOn_of_deriv_neg convex_univ
      (fun z _ => (differentiableAt_of_deriv_ne_zero (hf' z).ne).differentiableWithinAt.continuousWithinAt) fun x _ =>
      hf' x

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