OAI/Geometry/CylinderCovering/Footprints/Polygon.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.Footprints.radialReflection_apply line 10
2. lemma OAI.CylinderCovering.Footprints.radialReflection_involutive line 13
3. lemma OAI.CylinderCovering.Footprints.radialReflection_injective line 17
4. theorem OAI.CylinderCovering.Footprints.absoluteFootprint_split line 20
5. theorem OAI.CylinderCovering.Footprints.absoluteFootprint_eq_union_hulls line 52
6. theorem OAI.CylinderCovering.Footprints.positiveAbsoluteVertices_injective line 67
7. theorem OAI.CylinderCovering.Footprints.negativeAbsoluteVertices_injective line 73
8. theorem OAI.CylinderCovering.Footprints.absoluteFootprint_piece_interiors_nonempty line 80
9. theorem OAI.CylinderCovering.Footprints.absolute_polygon_statement line 97
10. theorem OAI.CylinderCovering.Footprints.absoluteFootprint_piece_intersection line 103
11. theorem OAI.CylinderCovering.Footprints.absoluteFootprint_piece_intersection_volume line 134
12. theorem OAI.CylinderCovering.Footprints.absoluteArea_eq_piece_areas line 148
13. theorem OAI.CylinderCovering.Footprints.absoluteFootprint_image_eq_union_hulls line 158