OAI/Geometry/IsometricImmersion/Metrics/UniversalMetricQ.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.universalQDenominator line 12
  2. def OAI.SmoothLocal.HighEquation.universalMetricQ line 15
  3. def OAI.SmoothLocal.HighEquation.universalMetricQDomain line 20
  4. def OAI.SmoothLocal.HighEquation.universalMetricQTube line 23
  5. theorem OAI.SmoothLocal.HighEquation.universalQDenominator_metricPBundle line 26
  6. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_eq_universalMetricQ line 29
  7. theorem OAI.SmoothLocal.HighEquation.universalQDenominator_contDiffOn line 40
  8. theorem OAI.SmoothLocal.HighEquation.universalMetricQDomain_isOpen line 46
  9. theorem OAI.SmoothLocal.HighEquation.universalMetricQ_contDiffOn line 50
  10. theorem OAI.SmoothLocal.HighEquation.universalMetricQTube_isCompact line 64
  11. theorem OAI.SmoothLocal.HighEquation.universalMetricQTube_subset_domain line 73
  12. theorem OAI.SmoothLocal.HighEquation.universalMetricQTube_finite_bounds line 82