OAI/Geometry/CylinderCovering/Ruled/Local.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.ProductLocal.affineCell_dilation line 12
2. lemma OAI.CylinderCovering.ProductLocal.affine_logarithmicCell line 23
3. lemma OAI.CylinderCovering.ProductLocal.affine_logarithmicIntercept line 29
4. lemma OAI.CylinderCovering.ProductLocal.logarithmic_projectedCylinder_eq line 35
5. theorem OAI.CylinderCovering.ProductLocal.logarithmic_local_proof line 41
6. theorem OAI.CylinderCovering.ProductLocal.logarithmic_source_local line 65
7. theorem OAI.CylinderCovering.ProductLocal.complete_local_proof line 123