OAI/Geometry/SurfaceImmersion/Primitive/PreparedCircularDirections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The chosen generic phase covectors give nonvertical remaining directions at every crossing inside the current primitive disk.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.boundaryCrossingSet_eq_circular line 19
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.prepared_circular_direction_first line 32