antitoneOn_of_deriv_nonpos — Mathlib

English

If a differentiable function has derivative nonpositive everywhere, then the function is antitone (nonincreasing) on its domain (here, on R).

Русский

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

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 nonpositive, then
`f` is an antitone function on `D`. -/
theorem antitoneOn_of_deriv_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
    (hf' : DifferentiableOn ℝ f (interior D)) (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) : AntitoneOn f D :=
  fun x hx y hy hxy => by
  simpa only [zero_mul, sub_nonpos] using hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos x hx y hy hxy

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