OAI/Geometry/CylinderCovering/Footprints/Shapes.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.Footprints.absoluteFootprint_not_convex line 11
2. lemma OAI.CylinderCovering.Footprints.affineFootprint_half_eq_region line 16
3. lemma OAI.CylinderCovering.Footprints.affineFootprint_half_eq_convexHull line 24
4. lemma OAI.CylinderCovering.Footprints.affineFootprint_half_vertices_independent line 31
5. lemma OAI.CylinderCovering.Footprints.affineFootprint_convex line 36
6. lemma OAI.CylinderCovering.Footprints.affineFootprint_interior_nonempty line 39
7. lemma OAI.CylinderCovering.Footprints.affineFootprint_boundary_mem line 66
8. lemma OAI.CylinderCovering.Footprints.affine_width_pos line 78
9. lemma OAI.CylinderCovering.Footprints.affineFootprint_eq_convexHull_trapezoid line 84
10. lemma OAI.CylinderCovering.Footprints.trapezoidVertices_injective line 164
11. lemma OAI.CylinderCovering.Footprints.trapezoid_vertical_sides line 174
12. lemma OAI.CylinderCovering.Footprints.affineFootprint_image_eq_convexHull line 184
13. lemma OAI.CylinderCovering.Footprints.trapezoid_image_vertices_injective line 191
14. theorem OAI.CylinderCovering.Footprints.footprint_shapes line 199