Simultaneous face-preserving rounding to parent vertices

Proved

Hirsch.face_preserving_vertex_selection

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

extreme-faceshirsch-conjecturepath-repairpolyhedra

Let P be a compact Euclidean polytope and let F_i be any family of closed extreme subsets of P. There is one selection r sending every feasible point of P to a parent vertex, fixing every existing parent vertex, such that membership in every supplied face is preserved simultaneously: x in F_i implies r(x) in F_i. The family of faces need not be finite; no continuity or adjacency preservation is asserted.

Preamble

import Mathlib
import Mathlib.Analysis.Convex.KreinMilman
import Definitions.Def_Hirsch_model

open scoped BigOperators RealInnerProductSpace
open Set Hirsch

Formal statement

namespace Hirsch

theorem face_preserving_vertex_selection
    {d : ℕ} {ι : Type*}
    (P : Set (EuclideanSpace ℝ (Fin d)))
    (F : ι → Set (EuclideanSpace ℝ (Fin d)))
    (hP : IsCompact P) (hF : ∀ i, IsExtreme ℝ P (F i))
    (hclosed : ∀ i, IsClosed (F i)) :
    ∃ r : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d),
      (∀ x ∈ P, r x ∈ extremePoints ℝ P) ∧
      (∀ x ∈ extremePoints ℝ P, r x = x) ∧
      (∀ i x, x ∈ F i → r x ∈ F i) := by sorry

end Hirsch

Source

Verified Lean theorem from jjoshua2/prove2me-work PR #50.

View graph