Least exposed faces and relative interior

This module proves the converse to Face.isLeastFaceAt_of_mem_relInterior. The proof works inside the affine span of a face. If the point is on the relative boundary, Hahn--Banach gives a nonconstant supporting functional there. After extension to the ambient space, a finite lexicographic perturbation of the functional exposing the original face produces a strictly smaller exposed face through the point, contradicting leastness.

theorem EGZ.RationalPolytope.Face.IsLeastFaceAt.mem_relInterior {d : ℕ} {P : RationalPolytope d} {q : RealCoord d} {F : P.Face} (hleast : IsLeastFaceAt P q F) : q ∈ F.relInterior

A least exposed face containing q contains q in its relative interior.