OAI/Geometry/CylinderCovering/Caps/FiniteGeometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.HalfheightFinite.halfwidth_nonneg line 13
2. lemma OAI.CylinderCovering.HalfheightFinite.midpoint_distance line 17
3. lemma OAI.CylinderCovering.HalfheightFinite.intercept_mem line 31
4. lemma OAI.CylinderCovering.HalfheightFinite.firstRaw_ne line 50
5. lemma OAI.CylinderCovering.HalfheightFinite.secondRaw_ne line 55
6. lemma OAI.CylinderCovering.HalfheightFinite.normalized_cylinder_mem line 60
7. lemma OAI.CylinderCovering.HalfheightFinite.first_intercept line 76
8. lemma OAI.CylinderCovering.HalfheightFinite.second_intercept line 83
9. lemma OAI.CylinderCovering.HalfheightFinite.first_member line 90
10. lemma OAI.CylinderCovering.HalfheightFinite.second_member line 114
11. theorem OAI.CylinderCovering.HalfheightFinite.finite_coverage line 138
12. lemma OAI.CylinderCovering.HalfheightFinite.firstAxis_unit line 165
13. lemma OAI.CylinderCovering.HalfheightFinite.secondAxis_unit line 170
14. theorem OAI.CylinderCovering.HalfheightFinite.cubic_finite_coverage line 175
15. theorem OAI.CylinderCovering.HalfheightFinite.fractional_finite_coverage line 182