rightDeriv_le_slope_of_mem_interior

English

For x ∈ interior S and y ∈ S with x<y, the right derivative at x is bounded above by slope f x y.

Русский

При x∈ interior S и y∈ S, x<y, правая производная в x не больше slope f x y.

LaTeX

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

Lean4

theorem rightDeriv_le_slope_of_mem_interior (hfc : ConvexOn ℝ S f) {y : ℝ} (hxs : x ∈ interior S) (hys : y ∈ S)
    (hxy : x < y) : derivWithin f (Ioi x) x ≤ slope f x y :=
  rightDeriv_le_slope hfc (interior_subset hxs) hys hxy (differentiableWithinAt_Ioi_of_mem_interior hfc hxs)

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