OAI/Geometry/ProjectionVolume/FiniteVertices.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper092.HPolytope.extreme_active_unique line 18
2. theorem OAI.Paper092.HPolytope.finite_extremePoints line 50
3. theorem OAI.Paper092.HPolytope.eq_convexHull_extremePoints line 64
4. theorem OAI.Paper092.halfspaces_are_finite_convex_hull line 77