OAI/Geometry/WeakMTW/Geodesics/IntrinsicUniqueness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.coordinate_germ_unique line 22
  2. def OAI.WeakMTWGlobalSupport.RiemannianLocal.curveState line 47
  3. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.curveState_continuous line 50
  4. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.curveState_congr line 59
  5. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.curveState_chart_deriv line 67
  6. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.intrinsic_germ_unique line 78
  7. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.tangentBundle_t2Space line 129
  8. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.intrinsic_global_unique line 145
  9. theorem OAI.WeakMTWGlobalSupport.WeakMTW.completeGeodesic_unique line 178