isExtreme_singleton — Mathlib

English

A singleton {x} is extreme in A iff x is an extreme point of A.

Русский

Подмножество {x} экстремально в A тогда, когда x является крайней точкой A.

LaTeX

$$$\IsExtreme 𝕜 A \{ x \} \quad\text{iff}\quad x \in A^{extremePoints}_{𝕜}$$$

Lean4

/-- x is an extreme point to A iff {x} is an extreme set of A. -/
@[simp]
theorem isExtreme_singleton : IsExtreme 𝕜 A { x } ↔ x ∈ A.extremePoints 𝕜 := by simp [isExtreme_iff, extremePoints]

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