OAI/Geometry/CylinderCovering/Singular/EdgeOneCover.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.SingularEdgeOneCover.height_eq line 13
2. def OAI.CylinderCovering.SingularEdgeOneCover.swap line 20
3. lemma OAI.CylinderCovering.SingularEdgeOneCover.map_eq_similarity line 35
4. lemma OAI.CylinderCovering.SingularEdgeOneCover.map_inverse line 40
5. lemma OAI.CylinderCovering.SingularEdgeOneCover.map_image_tetrahedron line 44
6. lemma OAI.CylinderCovering.SingularEdgeOneCover.map_image_lowerTip line 70
7. lemma OAI.CylinderCovering.SingularEdgeOneCover.map_image_upperTip line 90
8. lemma OAI.CylinderCovering.SingularEdgeOneCover.ceiling_eq line 110
9. lemma OAI.CylinderCovering.SingularEdgeOneCover.fieldP_eq line 114
10. lemma OAI.CylinderCovering.SingularEdgeOneCover.fieldQ_eq line 118
11. lemma OAI.CylinderCovering.SingularEdgeOneCover.label_dictionary line 123
12. lemma OAI.CylinderCovering.SingularEdgeOneCover.edgeU_label line 138
13. lemma OAI.CylinderCovering.SingularEdgeOneCover.edgeV_label line 144
14. lemma OAI.CylinderCovering.SingularEdgeOneCover.map_lower_parameter line 150
15. lemma OAI.CylinderCovering.SingularEdgeOneCover.map_upper_parameter line 159
16. lemma OAI.CylinderCovering.SingularEdgeOneCover.label_expand_contract line 168
17. lemma OAI.CylinderCovering.SingularEdgeOneCover.map_image_lowerFamily line 173
18. lemma OAI.CylinderCovering.SingularEdgeOneCover.map_image_upperFamily line 197
19. lemma OAI.CylinderCovering.SingularEdgeOneCover.half_ne line 221
20. lemma OAI.CylinderCovering.SingularEdgeOneCover.transport_carrier line 223
21. lemma OAI.CylinderCovering.SingularEdgeOneCover.transport_familySet line 227
22. lemma OAI.CylinderCovering.SingularEdgeOneCover.transport_zero_tendsto line 231
23. theorem OAI.CylinderCovering.SingularEdgeOneCover.alternative_cover line 242
24. theorem OAI.CylinderCovering.SingularEdgeOneCover.flexible_cover line 289
25. theorem OAI.CylinderCovering.SingularEdgeOneCover.exact_cover line 331