OAI/Geometry/IsometricImmersion/Coordinates/AffinePushforward.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.affineInverseCoordinates line 11
  2. theorem OAI.SmoothLocal.Geometry.affineInverseCoordinates_contDiff line 14
  3. theorem OAI.SmoothLocal.Geometry.affineInverseCoordinates_affineCoordinates line 19
  4. theorem OAI.SmoothLocal.Geometry.affineCoordinates_affineInverseCoordinates line 25
  5. def OAI.SmoothLocal.Geometry.affineCoordinateHomeomorph line 31
  6. def OAI.SmoothLocal.Geometry.affinePushforwardMetric line 40
  7. theorem OAI.SmoothLocal.Geometry.affinePullback_pushforward line 44
  8. theorem OAI.SmoothLocal.Geometry.affinePushforward_pullback line 57
  9. theorem OAI.SmoothLocal.Geometry.affinePullbackMetric_add line 70
  10. theorem OAI.SmoothLocal.Geometry.affinePullback_add_pushforward line 77
  11. theorem OAI.SmoothLocal.Geometry.affinePushforwardMetric_eq_zero_iff line 83
  12. theorem OAI.SmoothLocal.Geometry.affinePushforwardMetric_support line 96
  13. theorem OAI.SmoothLocal.Geometry.affinePushforwardMetric_tsupport line 115
  14. theorem OAI.SmoothLocal.Geometry.affinePushforwardMetric_tsupport_subset line 121
  15. theorem OAI.SmoothLocal.Geometry.affinePushforwardMetric_contDiff line 128