OAI/Geometry/CylinderCovering/Angular/TableConsequences.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.AngularTableCover.continuous_ceiling_cover line 12
2. theorem OAI.CylinderCovering.AngularTableCover.continuous_reciprocal_covers line 19
3. theorem OAI.CylinderCovering.AngularTableCover.squared_family_costs line 41
4. theorem OAI.CylinderCovering.AngularTableCover.cartesian_family_costs line 65
5. theorem OAI.CylinderCovering.AngularTableCover.reciprocal_midpoint_data line 93
6. theorem OAI.CylinderCovering.AngularTableCover.reciprocal_midpoint_lower_base line 98
7. theorem OAI.CylinderCovering.AngularTableCover.reciprocal_midpoint_upper_base line 109