OAI/Geometry/SurfaceImmersion/Primitive/PhaseCrossingTransversality.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Independent phase covectors give the nonzero first components of the actual transported directions at every finite crossing.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.firstCoordinateCovector line 16
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.firstCoordinateCovector_apply line 18
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phaseDerivative_fst line 26
  4. theorem OAI.ClosedSurfaceR4.phase_crossing_first_nonzero line 37