OAI/Geometry/CylinderCovering/Nilpotent/ShadowSimilarity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.Nilpotent.inner_coordinates line 12
2. lemma OAI.CylinderCovering.Nilpotent.centerDirection_inner line 19
3. lemma OAI.CylinderCovering.Nilpotent.centerDirection_norm line 23
4. lemma OAI.CylinderCovering.Nilpotent.centerDirection_involutive line 28
5. lemma OAI.CylinderCovering.Nilpotent.projection_centerMap line 32
6. lemma OAI.CylinderCovering.Nilpotent.projection_centerMap_image line 41
7. theorem OAI.CylinderCovering.Nilpotent.centerMap_shadowArea line 50
8. theorem OAI.CylinderCovering.Nilpotent.shadowSimilarity line 60