OAI/Geometry/IsometricImmersion/Calculus/QuotientCalculus.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.coordPartial_div line 16
  2. theorem OAI.SmoothLocal.Geometry.coordPartial_div_on line 35
  3. def OAI.SmoothLocal.Geometry.coordinateDrift line 44
  4. theorem OAI.SmoothLocal.Geometry.coordinateDrift_quotient line 47
  5. theorem OAI.SmoothLocal.Geometry.coordinateDrift_self_quotient line 57
  6. theorem OAI.SmoothLocal.Geometry.quotient_contDiffOn line 68
  7. def OAI.SmoothLocal.Geometry.explicitDriftError line 74
  8. theorem OAI.SmoothLocal.Geometry.explicitDriftError_contDiffOn line 77
  9. theorem OAI.SmoothLocal.Geometry.height_energy_quotient_pos line 89