OAI/Geometry/SurfaceImmersion/Primitive/ActualFiniteCrossingNormal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite crossing construction applied to the actual second form of one immersion, with its canonical transverse preferred normal.

  1. theorem OAI.ClosedSurfaceR4.GeometryPreservation.actual_finite_crossing_normal line 16