extremePoints_eq — Mathlib

English

If A is extreme in B, then B.extremePoints 𝕜 = B ∩ A.extremePoints 𝕜.

Русский

Если A крайнее в B, то B.extremePoints 𝕜 = B ∩ A.extremePoints 𝕜.

LaTeX

$$$\text{If } IsExtreme 𝕜 A B,\text{ then } B.extremePoints 𝕜 = B \cap A.extremePoints 𝕜$$$

Lean4

theorem extremePoints_eq (hAB : IsExtreme 𝕜 A B) : B.extremePoints 𝕜 = B ∩ A.extremePoints 𝕜 :=
  Subset.antisymm (fun _ hx ↦ ⟨hx.1, hAB.extremePoints_subset_extremePoints hx⟩)
    (inter_extremePoints_subset_extremePoints_of_subset hAB.1)

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