OAI/Geometry/WeakMTW/Coordinates/RadialLength.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakMTWGlobalSupport.RadialCoordinates.metric_nonneg line 18
2. theorem OAI.WeakMTWGlobalSupport.RadialCoordinates.hasDerivAt_regularized_radius line 24
3. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.base_mem line 46
4. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.normalAt_mem line 53
5. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.radial_derivative_bound line 58
6. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.radial_along_curve line 84