continuousOn_interior

Mathlib.Analysis.Convex.Continuous

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

English

If f is concave on C, then f is continuous on interior(C).

Русский

Если f вогнута на C, то она непрерывна на interior(C).

LaTeX

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

Lean4

theorem continuousOn_interior (hf : ConcaveOn ℝ C f) : ContinuousOn f (interior C) :=
  hf.locallyLipschitzOn_interior.continuousOn

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

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

Разделы

Аффилиация

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