absConvexHull_empty

Mathlib.Analysis.LocallyConvex.AbsConvex

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

English

absConvexHull 𝕜 ∅ = ∅.

Русский

absConvexHull 𝕜 пустого множества равна пустому.

LaTeX

$$$$ \\operatorname{absConvexHull}_{\\mathbb{k}}(\\emptyset) = \\emptyset. $$$$

Lean4

@[simp]
theorem absConvexHull_empty : absConvexHull 𝕜 (∅ : Set E) = ∅ :=
  AbsConvex.empty.absConvexHull_eq

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

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

Разделы

Аффилиация

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