OAI/Geometry/IsometricImmersion/Curvature/CurvatureFirstBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Geometry.riemannFirstBound line 12
2. def OAI.SmoothLocal.Geometry.curvatureNumeratorFirstBound line 14
3. def OAI.SmoothLocal.Geometry.curvatureFirstBound line 15
4. theorem OAI.SmoothLocal.Geometry.riemannFirstBound_nonneg line 19
5. theorem OAI.SmoothLocal.Geometry.curvatureFirstBound_nonneg line 24
6. theorem OAI.SmoothLocal.Geometry.riemann_coordinate_bound_one line 31
7. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_coordinate_bound_one line 59