convexHull_univ

Mathlib.Analysis.Convex.Hull

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

English

The convex hull of the whole space is the whole space: convexHull 𝕜 (univ) = univ.

Русский

Выпуклая оболочка всей пространства равна всему пространству: convexHull 𝕜(всего) = всего.

LaTeX

$$$ convexHull 𝕜 (univ : Set E) = univ $$$

Lean4

@[simp]
theorem convexHull_univ : convexHull 𝕜 (univ : Set E) = univ :=
  ClosureOperator.closure_top (convexHull 𝕜)

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

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

Разделы

Аффилиация

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