Theorems · Theorem · real analysis

StrictMonoOn.exists_slope_lt_deriv_aux

∀ {x y : ℝ} {f : ℝ → ℝ},
  ContinuousOn f (Set.Icc x y) →
    x < y →
      StrictMonoOn (deriv f) (Set.Ioo x y) →
        (∀ w ∈ Set.Ioo x y, deriv f w ≠ 0) → ∃ a ∈ Set.Ioo x y, (f y - f x) / (y - x) < deriv f a

Defined in

Mathlib.Analysis.Convex.Deriv

Cited by

1 results in Mathlib

Foundations

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