OAI/Geometry/PolarProducts/CanonicalCoordinates.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CanonicalLinear.E line 12
  2. def OAI.CanonicalLinear.coordinate line 14
  3. def OAI.CanonicalLinear.adaptedMap line 16
  4. theorem OAI.CanonicalLinear.adaptedMap_apply line 20
  5. theorem OAI.CanonicalLinear.adaptedMap_coordinate line 24
  6. theorem OAI.CanonicalLinear.adaptedMap_u line 28
  7. theorem OAI.CanonicalLinear.adaptedMap_injective line 32
  8. def OAI.CanonicalLinear.adapted line 49
  9. theorem OAI.CanonicalLinear.adapted_apply line 55
  10. theorem OAI.CanonicalLinear.adapted_first line 59
  11. theorem OAI.CanonicalLinear.adapted_inverse_single line 63
  12. def OAI.CanonicalLinear.cotangent line 69
  13. theorem OAI.CanonicalLinear.cotangent_apply line 74
  14. theorem OAI.CanonicalLinear.cotangent_preserves line 78
  15. theorem OAI.CanonicalLinear.cotangent_injective line 86
  16. theorem OAI.CanonicalLinear.cotangent_first line 97
  17. def OAI.UpperCoordinates.phaseForm line 121
  18. theorem OAI.UpperCoordinates.form_parts line 125
  19. theorem OAI.UpperCoordinates.form_parts_symm line 130
  20. def OAI.UpperCoordinates.targetCoordinates line 134
  21. theorem OAI.UpperCoordinates.targetCoordinates_preserves line 138
  22. theorem OAI.UpperCoordinates.targetCoordinates_injective line 145
  23. theorem OAI.UpperCoordinates.targetCoordinates_first line 149