starConvex_empty

Mathlib.Analysis.Convex.Star

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

English

For any x, the empty set is star-convex at x.

Русский

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

LaTeX

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

Lean4

theorem starConvex_empty (x : E) : StarConvex 𝕜 x ∅ := fun _ hy => hy.elim

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

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

Разделы

Аффилиация

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