OAI/Geometry/CylinderCovering/Caps/Geometry.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.CylinderCovering.HalfheightFinite.height_mem_Iccline 11 - theorem
OAI.CylinderCovering.HalfheightFinite.tetrahedron_eq_unitEdgeline 15 - theorem
OAI.CylinderCovering.HalfheightFinite.tetrahedron_similarityline 39 - theorem
OAI.CylinderCovering.HalfheightFinite.unit_edge_geometryline 45 - theorem
OAI.CylinderCovering.HalfheightFinite.isRegularTetrahedronline 69 - theorem
OAI.CylinderCovering.HalfheightFinite.minimum_arealine 73 - theorem
OAI.CylinderCovering.HalfheightFinite.strict_cost_iff_half_minimumline 77