strictAntiOn_of_deriv_neg — Mathlib

English

If the derivative f'(x) is negative for all x, then f is strictly antitone (strictly decreasing) on the domain under consideration (here, ℝ).

Русский

Если производная f'(x) отрицательна для всех x, то f строго антимонотална (строго убывает) на области, где применимо (здесь на ℝ).

LaTeX

$$$\forall x

Lean4

/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is negative, then
`f` is a strictly antitone function on `D`. -/
theorem strictAntiOn_of_deriv_neg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
    (hf' : ∀ x ∈ interior D, deriv f x < 0) : StrictAntiOn f D := fun x hx y => by
  simpa only [zero_mul, sub_lt_zero] using
    hD.image_sub_lt_mul_sub_of_deriv_lt hf
      (fun z hz => (differentiableAt_of_deriv_ne_zero (hf' z hz).ne).differentiableWithinAt) hf' x hx y

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