OAI/Geometry/NodalSets/Charts/MetricConnectionFamilyLemmas.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Geometry.metricConnection line 16
  2. lemma OAI.Yau.Geometry.metricConnection_eq line 22
  3. lemma OAI.Yau.Geometry.positive_metric_inverse_continuous line 30
  4. lemma OAI.Yau.Geometry.christoffelCovector_continuous line 43
  5. theorem OAI.Yau.Geometry.metricConnection_continuous line 50
  6. theorem OAI.Yau.Geometry.smooth_metric_connection_continuous line 57
  7. lemma OAI.Yau.Geometry.metric_derivative_symmetric line 71
  8. theorem OAI.Yau.Geometry.exists_normal_chart line 82