OAI/Geometry/IsometricImmersion/Coordinates/PatchGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Geometry.patchBox line 13
2. def OAI.SmoothLocal.Geometry.centralBox line 16
3. theorem OAI.SmoothLocal.Geometry.patchBox_subset_centralBox line 19
4. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_eventuallyEq_of_metric_eventuallyEq line 23
5. theorem OAI.SmoothLocal.Geometry.patch_smallCurvature_eventually_model line 29
6. theorem OAI.SmoothLocal.Geometry.patch_smallCurvature_model_firstJet line 51