OAI/Geometry/IsometricImmersion/Coordinates/CoordinateSwap.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.swapCoordinateIndex line 11
  2. def OAI.SmoothLocal.Geometry.coordinateSwapMatrix line 13
  3. def OAI.SmoothLocal.Geometry.coordinateSwap line 15
  4. def OAI.SmoothLocal.Geometry.swappedMetric line 17
  5. def OAI.SmoothLocal.Geometry.swappedHeight line 20
  6. theorem OAI.SmoothLocal.Geometry.swapCoordinateIndex_zero line 22
  7. theorem OAI.SmoothLocal.Geometry.swapCoordinateIndex_one line 23
  8. theorem OAI.SmoothLocal.Geometry.swapCoordinateIndex_involutive line 25
  9. theorem OAI.SmoothLocal.Geometry.coordinateSwap_apply line 29
  10. theorem OAI.SmoothLocal.Geometry.coordinateSwap_involutive line 35
  11. theorem OAI.SmoothLocal.Geometry.coordinateSwapMatrix_det line 40
  12. theorem OAI.SmoothLocal.Geometry.coordinateSwapMatrix_isUnit line 43
  13. theorem OAI.SmoothLocal.Geometry.coordinateSwap_contDiff line 47
  14. theorem OAI.SmoothLocal.Geometry.coordinateSwap_preimage_isOpen line 50
  15. theorem OAI.SmoothLocal.Geometry.swappedMetric_smoothPositive line 54
  16. theorem OAI.SmoothLocal.Geometry.swappedHeight_contDiffOn line 60
  17. theorem OAI.SmoothLocal.Geometry.swappedMetric_apply line 65
  18. theorem OAI.SmoothLocal.Geometry.swappedMetric_det line 73
  19. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_swappedMetric line 79
  20. theorem OAI.SmoothLocal.Geometry.christoffel_swappedMetric line 86
  21. theorem OAI.SmoothLocal.Geometry.coordPartial_swap_comp line 98
  22. theorem OAI.SmoothLocal.Geometry.second_coordPartial_swap_comp line 107
  23. theorem OAI.SmoothLocal.Geometry.covHessian_swappedMetric line 120
  24. theorem OAI.SmoothLocal.Geometry.heightEnergy_swappedMetric line 133