OAI/Geometry/SurfaceImmersion/Primitive/CompactTurnDichotomy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness converts the two limiting mechanisms at turns and away from turns into a single small-scale alternative.

  1. lemma OAI.ClosedSurfaceR4.GeometryPreservation.compact_away_from_turns line 11
  2. theorem OAI.ClosedSurfaceR4.GeometryPreservation.small_scale_turn_or_longitudinal line 31