OAI/Geometry/SurfaceImmersion/Whitney/CircularBoundaryArcs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compact boundary portions in another phase chart have actual smooth regular coordinate arcs, extended later only for parameter selection.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.coordinateTransition_derivative_injective line 14
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularArcDomain line 38
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularArc line 41
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularArcDomain_open line 44
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularArc_smooth line 49
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularArc_regular line 55
  7. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularArcCompact line 73
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularArcCompact_compact line 76
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularArcCompact_subset line 84
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularArcCompact_covers line 91