OAI/Geometry/CylinderCovering/Angular/CubicFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.Cubic.family_node_strict line 11
2. lemma OAI.CylinderCovering.Cubic.family_cap_pos line 17
3. def OAI.CylinderCovering.Cubic.lowerFamily4 line 23
4. def OAI.CylinderCovering.Cubic.upperFamily4 line 30
5. def OAI.CylinderCovering.Cubic.finiteFamily4 line 37
6. lemma OAI.CylinderCovering.Cubic.finiteFamily4_covers_of_coordinate_cover line 40
7. lemma OAI.CylinderCovering.Cubic.finiteFamily4_total line 60
8. lemma OAI.CylinderCovering.Cubic.finiteFamily4_prescribed line 81
9. theorem OAI.CylinderCovering.Cubic.finiteCover_proof line 88