OAI/Geometry/IsometricImmersion/Metrics/ModelMetric.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Model.quarterMatrix line 14
  2. theorem OAI.SmoothLocal.Model.quarterMatrix_isUnit line 16
  3. theorem OAI.SmoothLocal.Model.quarterCoordinates_eq line 21
  4. def OAI.SmoothLocal.Model.scaledModelCurvature line 27
  5. theorem OAI.SmoothLocal.Model.scaledModelCurvature_contDiff line 30
  6. theorem OAI.SmoothLocal.Model.scaledModelCurvature_bound line 36
  7. def OAI.SmoothLocal.Model.modelMetricDomain line 50
  8. theorem OAI.SmoothLocal.Model.modelMetricDomain_isOpen line 52
  9. theorem OAI.SmoothLocal.Model.modelMetricDomain_contains_model_square line 55
  10. def OAI.SmoothLocal.Model.constructedModelMetric line 64
  11. theorem OAI.SmoothLocal.Model.constructedModelMetric_spec line 68
  12. theorem OAI.SmoothLocal.Model.constructedModelMetric_central_curvature line 89