OAI/Geometry/ProjectionVolume/PolytopeFaceGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper092.HPolytope.projected_seam_null_left line 16
2. theorem OAI.Paper092.HPolytope.face_inter_surface_null line 49
3. theorem OAI.Paper092.HPolytope.exists_other_active_of_redundant line 71
4. theorem OAI.Paper092.HPolytope.redundant_face_surface_null line 99
5. theorem OAI.Paper092.HPolytope.redundant_faceArea_zero line 112
6. theorem OAI.Paper092.HPolytope.exists_strict_face_point_of_essential line 118