OAI/Geometry/SurfaceImmersion/Primitive/FiniteBoundaryCrossingSets.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact crossing sets for the remaining curves in a finite induction. The no-three-curves condition keeps these points off the next boundary.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.boundaryCrossingSet line 15
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.boundaryCrossingSet_finite line 19
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.boundaryCrossingSet_mono line 31
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.boundaryCrossingSet_pair line 37
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.boundaryCrossingSet_disjoint_next line 43
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteBoundaryGeometry_restrict_remaining line 57