differentiableWithinAt_Iio_of_mem_interior

English

If f is differentiable on a convex open set, then differentiable within Iio x.

Русский

Если f дифференцируема на выпуклом открытом множестве, то дифференцируема внутри Iio x.

LaTeX

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

Lean4

theorem differentiableWithinAt_Iio_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
    DifferentiableWithinAt ℝ f (Iio x) x :=
  (hfc.hasDerivWithinAt_sSup_slope_of_mem_interior hxs).differentiableWithinAt

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