OAI/Geometry/IsometricImmersion/Calculus/MetricTwoJet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Geometry.MetricJetCalculus.coordPartial_const_mul_at line 13
2. theorem OAI.SmoothLocal.Geometry.metric_inverse_derivative_identity line 20
3. theorem OAI.SmoothLocal.Geometry.inverseMetric_coordPartial_eq_of_firstJet line 44
4. theorem OAI.SmoothLocal.Geometry.christoffel_coordPartial_formula line 64
5. theorem OAI.SmoothLocal.Geometry.christoffel_eq_of_firstJet line 107
6. theorem OAI.SmoothLocal.Geometry.christoffel_coordPartial_eq_of_twoJet line 114
7. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_eq_of_twoJet line 129