OAI/Geometry/SurfaceImmersion/Geometry/CompactActualFrame.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact five-profile estimates give an actual orthonormal normal frame with the prescribed limiting coefficients for the exact immersion.

  1. def OAI.ClosedSurfaceR4.GeometryPreservation.secondFormFrameGeometry line 14
  2. theorem OAI.ClosedSurfaceR4.GeometryPreservation.compact_actual_frame_stability line 18