OAI/Geometry/CylinderCovering/Ruled/LocalGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.ProductLocal.frame_apply line 12
2. lemma OAI.CylinderCovering.ProductLocal.frame_norm_le line 18
3. lemma OAI.CylinderCovering.ProductLocal.frame_diagonal line 26
4. lemma OAI.CylinderCovering.ProductLocal.affineCell_distance line 34
5. lemma OAI.CylinderCovering.ProductLocal.intercept_identity line 44
6. theorem OAI.CylinderCovering.ProductLocal.uniform_intercept_containment line 65