Faces as hulls of lifted support points

The stored generators of a polytope need not be the stored lifted support. The support/polytope invariant nevertheless identifies every face with the convex hull of precisely the lifted support points lying on that face.

theorem EGZ.FlagDecomposition.face_eq_convexHull_liftedSupport {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : Γ.carrier = (convexHull ℝ) (IntCoord.real '' ↑({q ∈ Φ.liftedSupport x | q.real ∈ Γ.carrier}))

theorem EGZ.FlagDecomposition.liftedSupport_face_nonempty {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : {q ∈ Φ.liftedSupport x | q.real ∈ Γ.carrier}.Nonempty