Theorems · Theorem · real analysis

strictMonoOn_of_deriv_pos

∀ {D : Set ℝ}, Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ interior D, 0 < deriv f x) → StrictMonoOn 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 positive, then f is a strictly monotone function on D. Note that we don't require differentiability explicitly as it already implied by the derivative being strictly positive.

Defined in

Mathlib.Analysis.Calculus.Deriv.MeanValue

Cited by

9 results in Mathlib

Foundations

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