OAI/Geometry/SurfaceImmersion/Atlas/PhaseBoundaryCurve.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Fixed compact boundary curves and their actual second-form fields. The cutoff is chosen from the curve geometry, independently of any immersion.

  1. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve line 16
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.coordinate line 29
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.coordinate_continuous line 32
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.coordinate_compact line 37
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.cutoff_exists line 40
  6. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.cutoff line 56
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.cutoff_properties line 58
  8. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.second line 64
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.second_smooth line 68
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.second_eq line 74
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.second_transition line 82
  12. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.exterior_preservation line 119