OAI/Geometry/IsometricImmersion/Volterra/VolterraInverse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.ODE.curvatureVolterraCLM line 16
  2. theorem OAI.SmoothLocal.ODE.curvatureVolterraCLM_norm_le line 20
  3. theorem OAI.SmoothLocal.ODE.curvatureVolterraCLM_contDiff line 31
  4. theorem OAI.SmoothLocal.ODE.one_add_curvatureVolterra_isUnit line 40
  5. def OAI.SmoothLocal.ODE.volterraSolution line 53
  6. theorem OAI.SmoothLocal.ODE.volterraSolution_equation line 56
  7. theorem OAI.SmoothLocal.ODE.volterraSolution_unique line 66
  8. theorem OAI.SmoothLocal.ODE.volterraSolution_contDiffAt line 79
  9. theorem OAI.SmoothLocal.ODE.volterraSolution_family_contDiffOn line 95