OAI/Geometry/IsometricImmersion/Metrics/UniversalMetricP.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.HighEquation.MetricPInput line 15
  2. def OAI.SmoothLocal.HighEquation.universalConnection line 17
  3. def OAI.SmoothLocal.HighEquation.universalDenominator line 20
  4. def OAI.SmoothLocal.HighEquation.universalEnergy line 23
  5. def OAI.SmoothLocal.HighEquation.universalMetricP line 28
  6. def OAI.SmoothLocal.HighEquation.universalMetricBase line 33
  7. def OAI.SmoothLocal.HighEquation.universalMetricDomain line 34
  8. def OAI.SmoothLocal.HighEquation.metricPBundle line 37
  9. theorem OAI.SmoothLocal.HighEquation.universalConnection_metricPBundle line 42
  10. theorem OAI.SmoothLocal.HighEquation.universalDenominator_metricPBundle line 46
  11. theorem OAI.SmoothLocal.HighEquation.universalEnergy_metricPBundle line 49
  12. theorem OAI.SmoothLocal.HighEquation.sixVariableP_eq_universalMetricP line 52
  13. theorem OAI.SmoothLocal.HighEquation.universalMetricDet_contDiff line 63
  14. theorem OAI.SmoothLocal.HighEquation.universalMetricBase_isOpen line 68
  15. theorem OAI.SmoothLocal.HighEquation.universalConnection_contDiffAt line 71
  16. theorem OAI.SmoothLocal.HighEquation.universalDenominator_contDiffOn line 85
  17. theorem OAI.SmoothLocal.HighEquation.universalMetricDomain_isOpen line 91
  18. theorem OAI.SmoothLocal.HighEquation.universalEnergy_contDiff line 95
  19. theorem OAI.SmoothLocal.HighEquation.universalMetricP_contDiffOn line 101
  20. def OAI.SmoothLocal.HighEquation.universalMetricBaseTube line 115
  21. def OAI.SmoothLocal.HighEquation.universalMetricTube line 118
  22. theorem OAI.SmoothLocal.HighEquation.universalMetricBaseTube_isCompact line 121
  23. theorem OAI.SmoothLocal.HighEquation.universalMetricBaseTube_subset_base line 126
  24. theorem OAI.SmoothLocal.HighEquation.universalMetricTube_isCompact line 133
  25. theorem OAI.SmoothLocal.HighEquation.universalMetricTube_subset_domain line 142
  26. theorem OAI.SmoothLocal.HighEquation.universalMetricTube_finite_P_bounds line 151