locallyLipschitzOn

Mathlib.Analysis.Convex.Continuous

URI: https://scilib.ai/kg/mathlib#ConcaveOn.locallyLipschitzOn

English

For a concaveOn function on C, if C is open and nonempty, then f is locally Lipschitz on C.

Русский

Для функции выпукло-обратной на открытом непустом C функция локально липшицева на C.

LaTeX

$$$\\LocallyLipschitzOn C f$$$

Lean4

protected theorem locallyLipschitzOn (hC : IsOpen C) (hf : ConcaveOn ℝ C f) : LocallyLipschitzOn C f := by
  simpa using hf.neg.locallyLipschitzOn hC

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru