OAI/Geometry/CylinderCovering/Cubic/Similarity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubicSimilarity.area_double_sub line 13
2. lemma OAI.CubicSimilarity.projection_double_sub line 29
3. lemma OAI.CubicSimilarity.shadow_double_sub line 36
4. lemma OAI.CubicSimilarity.double_sub_point line 48
5. lemma OAI.CylinderCovering.Cubic.K4_eq_double_sub line 57
6. lemma OAI.CylinderCovering.Cubic.K4_shadow line 80
7. theorem OAI.CylinderCovering.Cubic.K4_projection_minimum line 85
8. lemma OAI.CylinderCovering.Cubic.K4_compact line 101
9. lemma OAI.CylinderCovering.Cubic.K4_edge_length line 105