locallyLipschitzOn_interior — Mathlib

English

Let C ⊆ E be a set and f: E → ℝ. If f is concave on C, then f is locally Lipschitz on interior(C).

Русский

Пусть C ⊆ E и f: E → ℝ. Если f вогнута на C, то она локально липшицева на interior(C).

LaTeX

$$$$\\operatorname{ConcaveOn}_{\\mathbb{R}}(C,f) \\Rightarrow \\operatorname{LocallyLipOn}(\\operatorname{interior} C) f.$$$$

Lean4

theorem locallyLipschitzOn_interior (hf : ConcaveOn ℝ C f) : LocallyLipschitzOn (interior C) f :=
  (hf.subset interior_subset hf.1.interior).locallyLipschitzOn isOpen_interior

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