exposedPoints_subset

Mathlib.Analysis.Convex.Exposed

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

English

Every exposed point of A is an extreme point of A.

Русский

Каждая экспонированная точка A также является её крайней точкой.

LaTeX

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

Lean4

theorem exposedPoints_subset : A.exposedPoints 𝕜 ⊆ A := fun _ hx => hx.1

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

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

Разделы

Аффилиация

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