OAI/Geometry/IsometricImmersion/Coordinates/AffinePullback.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.matrixContinuousLinear line 11
  2. theorem OAI.SmoothLocal.Geometry.matrixContinuousLinear_apply line 14
  3. def OAI.SmoothLocal.Geometry.affineCoordinates line 17
  4. def OAI.SmoothLocal.Geometry.affinePullbackMetric line 20
  5. def OAI.SmoothLocal.Geometry.affinePullbackImmersion line 24
  6. theorem OAI.SmoothLocal.Geometry.affineCoordinates_contDiff line 28
  7. theorem OAI.SmoothLocal.Geometry.affineCoordinates_hasFDerivAt line 32
  8. theorem OAI.SmoothLocal.Geometry.affineCoordinates_fderiv line 38
  9. theorem OAI.SmoothLocal.Geometry.affineCoordinates_zero line 42
  10. theorem OAI.SmoothLocal.Geometry.isOpen_affine_preimage line 45
  11. theorem OAI.SmoothLocal.Geometry.affine_comp_contDiffOn line 50
  12. theorem OAI.SmoothLocal.Geometry.fderiv_affine_comp_apply line 56
  13. theorem OAI.SmoothLocal.Geometry.matrix_pullback_bilinear line 64
  14. theorem OAI.SmoothLocal.Geometry.affinePullbackMetric_smoothPositive line 72
  15. theorem OAI.SmoothLocal.Geometry.affinePullbackImmersion_isometric line 92
  16. theorem OAI.SmoothLocal.Geometry.mulVec_injective_of_transpose_mul_eq_one line 107