isClosed_closedConvexHull

Mathlib.Analysis.Convex.Topology

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

English

For any set s, the closed convex hull of s is a closed set.

Русский

Для любого множества s замкнутая выпуклая оболочка s замкнута.

LaTeX

$$IsClosed (closedConvexHull 𝕜 s)$$

Lean4

theorem isClosed_closedConvexHull {s : Set E} : IsClosed (closedConvexHull 𝕜 s) :=
  ((closedConvexHull 𝕜).isClosed_closure s).2

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

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

Разделы

Аффилиация

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