OAI/Geometry/ProjectionVolume/FacetBijection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper092.HPolytope.face_eq_exposedFace line 17
2. theorem OAI.Paper092.HPolytope.face_isExposed line 34
3. theorem OAI.Paper092.HPolytope.exposed_facet_eq_unique_face line 39
4. theorem OAI.Paper092.HPolytope.finite_exposed_facets line 57