OAI/Geometry/SurfaceImmersion/Atlas/PlaneCommonCoordinate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A common linear plane coordinate is regular on either of two nonzero curve velocities, including the case of collinear opposite velocities.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeShearLinear line 12
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeShearLinear_apply line 16
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeShearLinear_bijective line 21
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeShearEquiv line 40
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.plane_second_ne_zero line 45
  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_common_plane_parameter line 53
  7. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_common_plane_coordinate line 75