OAI/Geometry/CylinderCovering/Caps/Symmetry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CylinderCovering.HalfheightFinite.familyIsometry line 11
2. def OAI.CylinderCovering.HalfheightFinite.familyTranslation line 25
3. lemma OAI.CylinderCovering.HalfheightFinite.secondRaw_isometry line 27
4. lemma OAI.CylinderCovering.HalfheightFinite.secondAxis_isometry line 32
5. lemma OAI.CylinderCovering.HalfheightFinite.secondFoot_isometry line 37
6. lemma OAI.CylinderCovering.HalfheightFinite.projection_neg_axis line 44
7. theorem OAI.CylinderCovering.HalfheightFinite.secondBase_transported line 48
8. theorem OAI.CylinderCovering.HalfheightFinite.secondBase_area_eq line 60
9. theorem OAI.CylinderCovering.HalfheightFinite.secondBase_properties_of_first line 68
10. theorem OAI.CylinderCovering.HalfheightFinite.totalArea_eq_twice_first line 84