OAI/Geometry/WeakMTW/Geodesics/CompleteExistence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.shifted_local_intrinsic line 22
2. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.intrinsic_extend_interval line 50
3. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.intrinsic_arbitrarily_long line 104
4. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.intrinsic_complete_exists line 136
5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.completeGeodesic_exists line 177
6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesicExistenceUniqueness line 184