OAI/Geometry/SurfaceImmersion/Atlas/PhaseTransverseDefiner.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A boundary transverse to a phase has a nonzero defining derivative in that phase's second coordinate.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phase_chart_transverse_definer_at line 15
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phase_chart_transverse_definer line 41
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circular_radius_phase_determinant line 59
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phase_chart_circular_definer line 73