extremePoints_singleton

Mathlib.Analysis.Convex.Extreme

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

← MathLib Explorer

English

The extreme points of a singleton {x} are exactly {x}.

Русский

Крайние точки множества {x} равны {x}.

LaTeX

$$$\{x\}^{extremePoints}_{𝕜} = \{x\}$$$

Lean4

@[simp]
theorem extremePoints_singleton : ({ x } : Set E).extremePoints 𝕜 = { x } :=
  extremePoints_subset.antisymm <| singleton_subset_iff.2 ⟨mem_singleton x, fun _ hx₁ _ _ _ ↦ hx₁⟩

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

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

Разделы

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

Аффилиация

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