OAI/Geometry/CylinderCovering/Convexity/CylinderBridge.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TriangularCovering.TriCylinder.toCylinder_axis line 12
2. theorem OAI.TriangularCovering.TriCylinder.toCylinder_base_image line 15
3. theorem OAI.TriangularCovering.TriCylinder.toCylinder_carrier line 26
4. theorem OAI.TriangularCovering.TriCylinder.toCylinder_area line 37
5. theorem OAI.TriangularCovering.TriCylinder.toCylinder_compact line 51
6. theorem OAI.RuledApproximation.Cylinder.shadowArea_eq_global line 60
7. theorem OAI.RuledApproximation.familyRelativeArea_eq_global line 77
8. theorem OAI.CylinderCovering.openCounterexample_of_compact line 85
9. theorem OAI.CylinderCovering.openCounterexample_of_triangular line 102
10. theorem OAI.CylinderCovering.regularOpen_of_regularTriangular line 132