OAI/Geometry/SurfaceImmersion/Primitive/CircularPhaseBoundaryCurve.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual coordinate circles as the fixed phase curves of the induction.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularPhaseBoundaryCurve line 17
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularPhaseBoundaryCurve_carrier line 47
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circular_closed_disk_phase_source line 58