OAI/Geometry/IsometricImmersion/Darboux/SwappedDarboux.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.jetXX line 11
  2. def OAI.SmoothLocal.Geometry.solvedDarbouxQ line 14
  3. theorem OAI.SmoothLocal.Geometry.jetConnection_swappedMetric line 17
  4. theorem OAI.SmoothLocal.Geometry.jetMixed_swappedMetric line 26
  5. theorem OAI.SmoothLocal.Geometry.jetYY_swappedMetric line 37
  6. theorem OAI.SmoothLocal.Geometry.jetEnergy_swappedMetric line 45
  7. theorem OAI.SmoothLocal.Geometry.jetNumerator_swappedMetric line 52
  8. theorem OAI.SmoothLocal.Geometry.solvedDarboux_swappedMetric line 61
  9. theorem OAI.SmoothLocal.Geometry.solvedDarbouxQ_eq_swappedP line 70
  10. theorem OAI.SmoothLocal.Geometry.jetXX_differentiableAt line 78
  11. theorem OAI.SmoothLocal.Geometry.coordPartial_jetXX line 84
  12. theorem OAI.SmoothLocal.Geometry.solvedDarbouxQ_first_variables_differentiableAt line 91
  13. theorem OAI.SmoothLocal.Geometry.solvedDarbouxQ_firstJet_expanded line 100
  14. theorem OAI.SmoothLocal.Geometry.solvedDarbouxQ_deriv_b line 124
  15. theorem OAI.SmoothLocal.Geometry.solvedDarbouxQ_deriv_c line 139
  16. theorem OAI.SmoothLocal.Geometry.jetXX_at_height line 156
  17. theorem OAI.SmoothLocal.Geometry.solvedDarbouxQ_at_height line 160
  18. theorem OAI.SmoothLocal.Geometry.darbouxDet_of_solvedQ_at_height line 181
  19. theorem OAI.SmoothLocal.Geometry.darbouxDet_iff_solvedQ_at_height line 202