OAI/Geometry/SurfaceImmersion/Atlas/PhaseTransitionVectors.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A later curve's transverse coordinate vector, transported to the current phase chart and extended smoothly from its compact overlap.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.fderiv_local_inverse_injective line 13
  2. theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_transverse_vector line 31