convex_convexHull

Mathlib.Analysis.Convex.Hull

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

English

The convex hull of any set is convex.

Русский

Гейдж-оболочка любого множества выпукла.

LaTeX

$$$\\text{Convex}(\\operatorname{convexHull}_{\\mathbb{K}}(s))$$$

Lean4

theorem convex_convexHull : Convex 𝕜 (convexHull 𝕜 s) :=
  (convexHull 𝕜).isClosed_closure s

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

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

Разделы

Аффилиация

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