locallyLipschitz — Mathlib

English

If f is convex on the entire space, then f is locally Lipschitz on the whole space.

Русский

Если f выпукла на всём пространстве, то она локально липшицева на всём пространстве.

LaTeX

$$$$\\operatorname{ConvexOn}_{\\mathbb{R}} to_univ f \\Rightarrow \\operatorname{LocallyLip} f.$$$$

Lean4

protected theorem locallyLipschitz (hf : ConvexOn ℝ univ f) : LocallyLipschitz f := by
  simpa using hf.locallyLipschitzOn_interior

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