slope_le_leftDeriv_of_mem_interior

English

Reformulation: slope between x and y is bounded above by the left-derivative at y under appropriate hypotheses.

Русский

Переформулирование: наклон между x и y ограничен левой производной в y.

LaTeX

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

Lean4

theorem slope_le_leftDeriv_of_mem_interior (hfc : ConvexOn ℝ S f) (hys : x ∈ S) (hxs : y ∈ interior S) (hxy : x < y) :
    slope f x y ≤ derivWithin f (Iio y) y :=
  slope_le_leftDeriv hfc hys (interior_subset hxs) hxy (differentiableWithinAt_Iio_of_mem_interior hfc hxs)

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