OAI/Geometry/CylinderCovering/Angular/CubicScaledFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CylinderCovering.Cubic.scaledLowerFamily line 9
2. def OAI.CylinderCovering.Cubic.scaledUpperFamily line 16
3. def OAI.CylinderCovering.Cubic.scaledFiniteFamily line 23
4. lemma OAI.CylinderCovering.Cubic.scaledFiniteFamily_covers line 26
5. lemma OAI.CylinderCovering.Cubic.scaledFiniteFamily_total line 72
6. lemma OAI.CylinderCovering.Cubic.scaled_count_eq line 93
7. lemma OAI.CylinderCovering.Cubic.scaled_cap_eq line 98
8. lemma OAI.CylinderCovering.Cubic.scaledFiniteFamily_prescribed line 104
9. lemma OAI.CylinderCovering.Cubic.scaledLowerInterceptVertices_contraction line 111
10. lemma OAI.CylinderCovering.Cubic.scaledUpperInterceptVertices_contraction line 118
11. theorem OAI.CylinderCovering.Cubic.scaledFiniteCover_proof line 125