English
Characterization: x is an extreme point of A iff x ∈ A and for all x1,x2 ∈ A, if x lies in the open segment (x1,x2), then x1 = x and x2 = x.
Русский
Характеризация: x — крайняя точка A тогда и только тогда, когда x ∈ A и для любых x1,x2 ∈ A, если x лежит на открытом отрезке (x1,x2), то x1 = x и x2 = x.
LaTeX
$$$x \in A^{extremePoints}_{𝕜} \iff x \in A \land \forall x_1 \in A, \forall x_2 \in A, x \in openSegment 𝕜 x_1 x_2 \Rightarrow x_1 = x \land x_2 = x$$$
Lean4
/-- A point `x` is an extreme point of a set `A`
iff `x ∈ A` and for any `x₁`, `x₂` such that `x` belongs to the open segment `(x₁, x₂)`,
we have `x₁ = x`. -/
theorem mem_extremePoints_iff_left :
x ∈ A.extremePoints 𝕜 ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x :=
.rfl
