OAI/Geometry/SurfaceImmersion/Primitive/PhaseCircularPeriod.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The analytic profile attached to an atlas phase chart is exactly one of the real circular profiles used in the finite boundary construction.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseRealChartMap_comp_base line 19
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.geometric_profile_congr line 24
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_circular_geometric_profile line 34
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_circular_period_profile line 64