Theorems · Theorem · real analysis

antitoneOn_of_hasDerivWithinAt_nonpos

∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f f' : ℝ → ℝ},
      ContinuousOn f D →
        (∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) → (∀ x ∈ interior D, f' x ≤ 0) → AntitoneOn f D

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.

Defined in

Mathlib.Analysis.Calculus.Deriv.MeanValue

Cited by

0 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound