OAI/Geometry/ProjectionVolume/FacetExhaustiveness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper092.inner_eq_of_mem_intrinsicInterior line 16
2. theorem OAI.Paper092.HPolytope.exists_active_of_mem_exposedFace line 50
3. theorem OAI.Paper092.HPolytope.exposedFace_eq_face line 63