OAI/Geometry/NodalSets/Charts/MetricJetAdmissibility.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Yau.Geometry.MetricJet line 14
2. def OAI.Yau.Geometry.jetGradient line 17
3. def OAI.Yau.Geometry.jetHessian line 20
4. def OAI.Yau.Geometry.JetAdmissible line 24
5. lemma OAI.Yau.Geometry.jetGradient_continuousAt line 30
6. lemma OAI.Yau.Geometry.jetHessian_continuousAt line 37
7. theorem OAI.Yau.Geometry.jetAdmissible_eventually line 47
8. lemma OAI.Yau.Geometry.jetAdmissible_actual line 58