OAI/Geometry/SurfaceImmersion/Primitive/PrimitivePatchCurves.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual remaining boundary curves and finite crossing points inside a constructed primitive patch.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.coordinate_mem_compact line 22
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.coordinate_mem_region line 29
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.curve line 35
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.curve_compact line 37
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.curve_region line 41
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.curve_compact_coordinates line 46
  7. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.curve_coefficients line 51
  8. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.innerCrossings line 60
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.innerCrossings_finite line 63
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.innerCrossings_positive line 67
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.innerCrossings_region line 72
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SupportedPrimitivePatch.innerCrossings_compact_coordinates line 77