OAI/Geometry/CylinderCovering/Cubic/Contraction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CylinderCovering.Cubic.identityIsometry line 15
2. lemma OAI.CylinderCovering.Cubic.contraction_point line 17
3. lemma OAI.CylinderCovering.Cubic.contraction_double_sub line 22
4. lemma OAI.CylinderCovering.Cubic.contraction_K4 line 30
5. def OAI.CylinderCovering.Cubic.contractCylinder line 37
6. lemma OAI.CylinderCovering.Cubic.contractCylinder_axis line 55
7. lemma OAI.CylinderCovering.Cubic.contractCylinder_carrier line 57
8. lemma OAI.CylinderCovering.Cubic.contractCylinder_area line 62
9. lemma OAI.CylinderCovering.Cubic.contractFamily_covers line 70
10. lemma OAI.CylinderCovering.Cubic.contractFamily_total line 80
11. theorem OAI.CylinderCovering.Cubic.rescaledFiniteCover_proof line 84