English
Definition of extreme points: x ∈ A is extreme if it does not lie in any open segment with endpoints in A unless that segment is trivial.
Русский
Определение крайних точек: точка x ∈ A является крайней, если она не лежит на открытом отрезке между точками из A, кроме тривиального отрезка x–x.
LaTeX
$$$$ x \in A.extremePoints 𝕜 \iff x \in A \land \forall x_1,x_2 \in A, x \in openSegment 𝕜 x_1 x_2 \Rightarrow x_1 = x. $$$$
Lean4
/-- A point `x` is an extreme point of a set `A` if `x` belongs to no open segment with ends in
`A`, except for the obvious `openSegment x x`. -/
def extremePoints (A : Set E) : Set E :=
{x ∈ A | ∀ ⦃x₁⦄, x₁ ∈ A → ∀ ⦃x₂⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x}
