OAI/Geometry/WeakMTW/Coordinates/NormalLength.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.coordinateLength line 19
2. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.regularized_radius_length line 22
3. theorem OAI.WeakMTWGlobalSupport.NormalNeighborhood.NormalFlow.radial_length line 57