Prove2Me

Closed extreme faces with no shared parent extreme point are disjoint

Proved
Hirsch.closed_extreme_faces_disjoint_of_no_shared_parent_extreme

by jjosh · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

formalizationgraph-diameterpolyhedra

Let P be a compact subset of finite-dimensional Euclidean space, and let F and G be closed extreme subsets of P. If no extreme point of P belongs to both F and G, then F and G are disjoint. Equivalently, any nonempty intersection of two closed extreme faces of a compact parent contains a parent extreme point.

Preamble
import Mathlib
import Mathlib.Analysis.Convex.KreinMilman
open scoped RealInnerProductSpace
open Set
Formal statement
namespace Hirsch
theorem closed_extreme_faces_disjoint_of_no_shared_parent_extreme
    {d : ℕ}
    (P F G : Set (EuclideanSpace ℝ (Fin d)))
    (hP : IsCompact P)
    (hF : IsExtreme ℝ P F) (hG : IsExtreme ℝ P G)
    (hFc : IsClosed F) (hGc : IsClosed G)
    (hno : ¬ ∃ v : EuclideanSpace ℝ (Fin d),
      v ∈ Set.extremePoints ℝ P ∧ v ∈ F ∧ v ∈ G) :
    Disjoint F G := by sorry
end Hirsch
Source
https://github.com/jjoshua2/prove2me-work/commit/fb1594e865b723ea2e6bf63baf46beeba7025027 ; standalone Lean/Axiom gate Actions run 34699009349

View graph