OAI/Geometry/SurfaceImmersion/Atlas/SphericalCoordinateSecondForm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Linear chart coordinates preserve the actual second normal projection.

  1. lemma OAI.ClosedSurfaceR4.spherical_secondForm_coordinates line 12