exposedPoints_subset_extremePoints

Mathlib.Analysis.Convex.Exposed

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

← MathLib Explorer

English

The exposed points of A are contained in its extreme points.

Русский

Экспонированные точки A подпадают под экстремальные точки A.

LaTeX

$$$$ A.exposedPoints 𝕜 \subseteq A.extremePoints 𝕜. $$$$

Lean4

theorem exposedPoints_subset_extremePoints : A.exposedPoints 𝕜 ⊆ A.extremePoints 𝕜 := fun _ hx =>
  (mem_exposedPoints_iff_exposed_singleton.1 hx).isExtreme.mem_extremePoints

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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