OAI/Geometry/SmoothYau/Smoothness/FderivMetricPairing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.fderiv_metric_pairing line 24
2. lemma OAI.YauCounterexamples.fderiv_fderiv_apply line 33
3. lemma OAI.YauCounterexamples.fderiv_induced_metric line 40
4. lemma OAI.YauCounterexamples.induced_metric_christoffel line 58
5. lemma OAI.YauCounterexamples.sphere_immersion_normal_first line 75
6. lemma OAI.YauCounterexamples.sphere_immersion_normal_second line 87
7. theorem OAI.YauCounterexamples.sphere_immersion_gauss line 102