convexHull_empty

Mathlib.Analysis.Convex.Hull

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

English

The convex hull of the empty set is the empty set: convexHull 𝕜 (∅ : Set E) = ∅.

Русский

Выпуклая оболочка пустого множества равна пустому множеству.

LaTeX

$$$ convexHull 𝕜 (\\emptyset : Set E) = \\emptyset $$$

Lean4

@[simp]
theorem convexHull_empty : convexHull 𝕜 (∅ : Set E) = ∅ :=
  convex_empty.convexHull_eq

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

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

Разделы

Аффилиация

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