English
If F is nonempty and every B ∈ F is extreme in A, then A is extreme in the intersection of all B ∈ F.
Русский
Если F непусто и каждое B ∈ F является крайним в A, то A крайнее в пересечение всех B ∈ F.
LaTeX
$$$F\neq \emptyset \to (\forall B \in F, IsExtreme 𝕜 A B) \Rightarrow IsExtreme 𝕜 A (\bigcap F)$$$
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` and `x₂ = x`.
We used to use the RHS as the definition of `extremePoints`.
However, the conclusion `x₂ = x` is redundant,
so we changed the definition to the RHS of `mem_extremePoints_iff_left`. -/
theorem mem_extremePoints :
x ∈ A.extremePoints 𝕜 ↔ x ∈ A ∧ ∀ᵉ (x₁ ∈ A) (x₂ ∈ A), x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x :=
by
refine
⟨fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ ⟨h.2 hx₁ hx₂ hx, ?_⟩⟩, fun h ↦
⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ (h.2 x₁ hx₁ x₂ hx₂ hx).1⟩⟩
apply h.2 hx₂ hx₁
rwa [openSegment_symm]
