slope_le_leftDeriv — Mathlib

English

Under differentiability on Iio y, the slope is bounded above by the left-derivative at y.

Русский

При дифференцируемости на Iio y наклон не превосходит левую производную в y.

LaTeX

$$$$ \ slope f x y \le \ derivWithin f( Iio y ) y $$$$

Lean4

/-- Reformulation of `ConvexOn.slope_le_of_hasDerivWithinAt_Iio` using `derivWithin`. -/
theorem slope_le_leftDeriv (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : DifferentiableWithinAt ℝ f (Iio y) y) : slope f x y ≤ derivWithin f (Iio y) y :=
  hfc.slope_le_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

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