OAI/Geometry/SurfaceImmersion/Atlas/FinitePhaseCurveDefiners.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite boundary defining functions pulled through an actual nonlinear phase chart. Crossings and phase tangencies are the only exceptions.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.finite_phase_curve_definers line 14