OAI/Geometry/NodalSets/Charts/InverseMetricJet.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Geometry.form_derivative_zero line 12
2. lemma OAI.Yau.Geometry.inverse_fderiv_zero line 21
3. lemma OAI.Yau.Geometry.orthonormal_inverse_axis line 36
4. lemma OAI.Yau.Geometry.pulledForm_slice_smooth line 51
5. def OAI.Yau.Geometry.inverseChartCoeff line 58
6. theorem OAI.Yau.Geometry.actual_inverse_metric_normal_jets line 64