OAI/Geometry/SurfaceImmersion/Primitive/SurfaceCircularThreshold.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Freeze the circular coefficient bounds on the original surface before choosing its supported angle and its smaller jet neighborhood.

  1. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.surfaceCircularProfile line 14
  2. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.compact_surface_circular_threshold line 23
  3. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.surfaceCircularProfile_turn_iff line 77