OAI/Geometry/CylinderCovering/Nilpotent/ShadowConsequences.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.Nilpotent.centerMap_shadowArea_range line 9
2. theorem OAI.CylinderCovering.Nilpotent.centerMap_minimumShadowArea line 25
3. theorem OAI.CylinderCovering.Nilpotent.centerMap_minimizingDirection_iff line 41
4. theorem OAI.CylinderCovering.Nilpotent.centerMap_minimumShadowArea_pos_iff line 53
5. theorem OAI.CylinderCovering.Nilpotent.centerMap_minimumShadowArea_zero_iff line 58