English
Let C be a subset of a normed space E and f: E → ℝ be defined on C. If f is convex on C, then f is locally Lipschitz on the interior of C; that is, for every point in interior(C) there exists a neighborhood on which f satisfies a Lipschitz condition.
Русский
Пусть C ⊆ E, где E — нормированное пространство, и f: E → ℝ определена на C. Если f выпукла на C, то она локально липшинцова на interior(C); то есть для каждой точки внутри interior(C) существует окрестность, на которой выполняется условие Липшица.
LaTeX
$$$$\\operatorname{ConvexOn}_{\\mathbb{R}}(C,f) \\Rightarrow \\operatorname{LocallyLipOn}(\\operatorname{interior} C) f.$$$$
Lean4
theorem locallyLipschitzOn_interior (hf : ConvexOn ℝ C f) : LocallyLipschitzOn (interior C) f :=
(hf.subset interior_subset hf.1.interior).locallyLipschitzOn isOpen_interior
