OAI/Geometry/IsometricImmersion/Immersions/InducedMetric.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.second_coordPartial_eq_fderiv line 16
  2. theorem OAI.SmoothLocal.Geometry.coordPartial_comm line 27
  3. def OAI.SmoothLocal.Geometry.inducedMetric line 38
  4. theorem OAI.SmoothLocal.Geometry.inducedMetric_eq_of_isometric line 41
  5. theorem OAI.SmoothLocal.Geometry.metric_partial_eq line 48
  6. theorem OAI.SmoothLocal.Geometry.second_partial_inner_tangent line 69