OAI/Geometry/WeakMTW/Geodesics/LocalFanVariation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFan_smooth_on line 22
2. theorem OAI.WeakMTWGlobalSupport.WeakMTW.localFanDomain_open line 32
3. theorem OAI.WeakMTWGlobalSupport.WeakMTW.fanCoordinates_smooth_on line 38
4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.fanMomentum_coord_on line 48
5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.fanMomentum_hasDerivAt_on line 71
6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.fanMomentum_affine_on line 105