slope_lt_leftDeriv — Mathlib

English

Let S be a domain where f is strictly convex. If x<y and f is differentiable from the left at y, then the slope from x to y is strictly less than the left derivative at y.

Русский

Пусть f строго выпуклая на области S. При x<y и наличии левой производной в y, наклон секанта меньше левой производной в y.

LaTeX

$$$\text{If } x

Lean4

theorem slope_lt_leftDeriv (hfc : StrictConvexOn ℝ 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_lt_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

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