OAI/Geometry/WeakMTW/Coordinates/LocalDistance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWGlobalSupport.RiemannianLocal.normalChart line 24
2. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.normalChart_apply line 29
3. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.normalChart_source line 34
4. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.normalChart_zero line 40
5. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.normalChart_target_center line 46
6. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.edist_normalChart_le line 53
7. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.radial_path_length line 79
8. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.normal_distance_of_ball line 103