OAI/Geometry/SurfaceImmersion/Primitive/PreparedPointCrossings.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Initial crossing inequalities in every chart through a prepared point. The curvature is the actual curvature of the scaled induced metric.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.prepared_point_crossings line 19