extremePoints_subset

Mathlib.Analysis.Convex.Extreme

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

English

For any set A, the set of extreme points of A is a subset of A.

Русский

Для любого множества A множество его экстремальных точек является подмножеством A.

LaTeX

$$$$ \\operatorname{extremePoints}_{\\mathbb{K}}(A) \\subseteq A. $$$$

Lean4

theorem extremePoints_subset : A.extremePoints 𝕜 ⊆ A := fun _ hx ↦ hx.1

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

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

Разделы

Аффилиация

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