locallyLipschitz — Mathlib

English

If f is concave on univ, then f is locally Lipschitz on the whole space.

Русский

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

LaTeX

$$$$\\operatorname{ConcaveOn}_{\\mathbb{R}} \\mathrm{univ} f \\Rightarrow \\operatorname{LocallyLip} f.$$$$

Lean4

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

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