slope_le_derivWithin — Mathlib

English

Reformulation: slope ≤ derivWithin f on a given side.

Русский

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

LaTeX

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

Lean4

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

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