OAI/Geometry/WeakMTW/Coordinates/RadialCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWGlobalSupport.RadialCoordinates.fiber line 20
2. def OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.normalAt line 70
3. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.normalAt_apply line 74
4. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.normalAt_source line 79
5. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.normalAt_target line 83
6. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.normalAt_smooth line 87
7. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.normalAt_inverse_smooth line 95
8. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.normalAt_gauss line 99
9. theorem OAI.WeakMTWGlobalSupport.RadialCoordinates.metric_cauchy_sq line 136