starConvex_univ

Mathlib.Analysis.Convex.Star

URI: https://scilib.ai/kg/mathlib#starConvex_univ

English

For any x, the whole space is star-convex at x.

Русский

Для любой точки x всё пространство является звездообразно выпуклым относительно x.

LaTeX

$$$$StarConvex_{\mathbb{K}}(x, \mathsf{univ}).$$$$

Lean4

theorem starConvex_univ (x : E) : StarConvex 𝕜 x univ := fun _ _ _ _ _ _ _ => trivial

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

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

Разделы

Аффилиация

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