OAI/Geometry/SurfaceImmersion/Atlas/PreparedPointCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A prepared spherical point has the exact radial second form in its selected atlas chart, using a genuine smooth representative of the chart map.

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