convexHull_eq_self

Mathlib.Analysis.Convex.Hull

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

English

The convex hull of a set s equals s if and only if s is convex.

Русский

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

LaTeX

$$$ convexHull 𝕜 s = s \\iff Convex 𝕜 s $$$

Lean4

theorem convexHull_eq_self : convexHull 𝕜 s = s ↔ Convex 𝕜 s :=
  (convexHull 𝕜).isClosed_iff.symm

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

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

Разделы

Аффилиация

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