deriv_le_slope — Mathlib

English

For differentiable at x, the derivative at x is bounded above by the slope to y.

Русский

Если f дифференцируема в x, то производная в x не превосходит наклон к y.

LaTeX

$$$$ \ deriv f x \le \ slope f x y $$$$

Lean4

/-- Reformulation of `ConvexOn.le_slope_of_hasDerivAt` using `deriv` -/
theorem deriv_le_slope (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : DifferentiableAt ℝ f x) :
    deriv f x ≤ slope f x y :=
  le_slope_of_hasDerivAt hfc hx hy hxy hfd.hasDerivAt

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