OAI/Geometry/CylinderCovering/Radial/EqualityCover.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CylinderCovering.RadialEqualityCover.identityIsometry line 11
2. lemma OAI.CylinderCovering.RadialEqualityCover.scale_height line 13
3. lemma OAI.CylinderCovering.RadialEqualityCover.tetrahedron_eq_dilation line 16
4. lemma OAI.CylinderCovering.RadialEqualityCover.firstBase_eq_dilation line 49
5. lemma OAI.CylinderCovering.RadialEqualityCover.secondBase_eq_dilation line 69
6. def OAI.CylinderCovering.RadialEqualityCover.cylinders line 78
7. lemma OAI.CylinderCovering.RadialEqualityCover.cylinders_axis_zero line 82
8. lemma OAI.CylinderCovering.RadialEqualityCover.cylinders_axis_one line 85
9. lemma OAI.CylinderCovering.RadialEqualityCover.cylinders_base_zero line 88
10. lemma OAI.CylinderCovering.RadialEqualityCover.cylinders_base_one line 97
11. lemma OAI.CylinderCovering.RadialEqualityCover.cylinders_cover line 106
12. lemma OAI.CylinderCovering.RadialEqualityCover.first_covers_nonnegative line 114
13. lemma OAI.CylinderCovering.RadialEqualityCover.secondBase_mem_iff line 128
14. lemma OAI.CylinderCovering.RadialEqualityCover.second_covers_nonpositive line 142
15. lemma OAI.CylinderCovering.RadialEqualityCover.cylinders_area_each line 156
16. lemma OAI.CylinderCovering.RadialEqualityCover.cylinders_totalArea line 161
17. lemma OAI.CylinderCovering.RadialEqualityCover.cylinders_shadow_each line 164
18. lemma OAI.CylinderCovering.RadialEqualityCover.cylinders_relativeCost line 177
19. theorem OAI.CylinderCovering.RadialEqualityCover.equality_cover line 184