OAI/Geometry/SurfaceImmersion/Primitive/CompactCrossingPreservation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform positivity at the later crossings from the actual two second-form limits. Only the limiting angular speed and mixed component enter compactness.

  1. theorem OAI.ClosedSurfaceR4.GeometryPreservation.compact_crossing_preservation line 12