OAI/Geometry/SurfaceImmersion/Atlas/CompactPhaseCurveVectors.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth direction coefficients for the actual pieces of later curves inside one fixed primitive disk.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.inPhase line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.inPhase_compact line 22
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.inPhase_transition_target line 30
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.coordinate_transition line 44
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.inPhase_direction_coefficients line 53