OAI/Geometry/IsometricImmersion/Metrics/MetricCompatibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.metric_compatibility line 17
  2. theorem OAI.SmoothLocal.Geometry.metricDet_coordPartial line 36
  3. theorem OAI.SmoothLocal.Geometry.metricDet_partial_trace line 54
  4. theorem OAI.SmoothLocal.Geometry.metricDet_partial_y line 62
  5. theorem OAI.SmoothLocal.Geometry.heightEnergy_polynomial_symm line 69
  6. theorem OAI.SmoothLocal.Geometry.CompatibilityCalculus.coordPartial_quadratic line 80
  7. theorem OAI.SmoothLocal.Geometry.coordPartial_heightEnergy_polynomial line 103
  8. theorem OAI.SmoothLocal.Geometry.coordPartial_heightEnergy line 146
  9. theorem OAI.SmoothLocal.Geometry.heightEnergy_y_quotient line 162