antitone_of_deriv_nonpos — Mathlib

English

If a differentiable function has strictly negative derivative everywhere, then it is strictly antitone (strictly decreasing) on its domain (here, R).

Русский

Если производная функции строго отрицательна повсюду, то функция строго антимононна на своей области (R).

LaTeX

$$$\forall x

Lean4

/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonpositive, then
`f` is an antitone function. -/
theorem antitone_of_deriv_nonpos {f : ℝ → ℝ} (hf : Differentiable ℝ f) (hf' : ∀ x, deriv f x ≤ 0) : Antitone f :=
  antitoneOn_univ.1 <|
    antitoneOn_of_deriv_nonpos convex_univ hf.continuous.continuousOn hf.differentiableOn fun x _ => hf' x

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