rightDeriv_le_slope — Mathlib

English

Reformulation: the right derivative is bounded above by the slope.

Русский

Переформулирование: правая производная не превосходит наклон секанты.

LaTeX

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

Lean4

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

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