OAI/Geometry/NodalSets/Charts/LocalMetricJetContinuityLemmas.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Yau.Geometry.metric_inverse_continuousAt line 16
  2. lemma OAI.Yau.Geometry.metric_connection_continuousAt line 27
  3. lemma OAI.Yau.Geometry.localMetricGradient_continuousAt line 40
  4. lemma OAI.Yau.Geometry.localMetricHessian_continuousAt line 45
  5. def OAI.Yau.Geometry.linearCovectorPull line 61
  6. def OAI.Yau.Geometry.linearMetricPull line 64
  7. lemma OAI.Yau.Geometry.linearCovectorPull_apply line 68
  8. lemma OAI.Yau.Geometry.linearMetricPull_apply line 71
  9. def OAI.Yau.Geometry.linearMetricField line 74
  10. lemma OAI.Yau.Geometry.linearMetricField_positive line 77
  11. lemma OAI.Yau.Geometry.linearMetricField_fderiv line 84
  12. lemma OAI.Yau.Geometry.linearMetricField_fderiv_apply line 91
  13. lemma OAI.Yau.Geometry.linearScalar_fderiv line 96
  14. lemma OAI.Yau.Geometry.localMetricGradient_pair line 103
  15. lemma OAI.Yau.Geometry.linearMetricField_gradient line 114
  16. lemma OAI.Yau.Geometry.metricConnection_pair line 126
  17. lemma OAI.Yau.Geometry.linearMetricField_connection line 132