OAI/Geometry/SurfaceImmersion/Atlas/CoordinateTransverseDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The transverse coordinate derivative never vanishes at a rank-one crosscap whose longitudinal coordinate is the kernel.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.horizontal_ne_zero_of_vertical_zero line 15
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.coordinate_representative_derivative_ne_zero line 28