hasDerivWithinAt_rightDeriv_of_mem_interior

English

If f is convex on a convex set and x is interior, the right derivative exists and matches the derivative within Ioi x.

Русский

Если f выпукла на выпуклом множестве и x внутри, правая производная существует и равна внутри Ioi x.

LaTeX

$$$\\forall S f x,\\; \\text{ConvexOn } \\mathbb{R} \\; S \\; f \\Rightarrow x \\in \\mathrm{intr}(S) \\Rightarrow \\text{HasDerivWithinAt } f (\\mathrm{derivWithin}(f, \\mathrm{Ioi}(x), x)) (\\mathrm{Ioi}(x)) x.$$

Lean4

theorem hasDerivWithinAt_rightDeriv_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
    HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ioi x) x :=
  (hfc.differentiableWithinAt_Ioi_of_mem_interior hxs).hasDerivWithinAt

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