OAI/Geometry/WeakMTW/Geodesics/GlobalFlow.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFlow_smooth_fixedline 21 - theorem
OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFlow_smoothline 63 - theorem
OAI.WeakMTWGlobalSupport.WeakMTW.exp_total_smoothline 80