OAI/Geometry/SurfaceImmersion/Whitney/NormalizedPairFilling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An actual normalized two-zero field, rather than an assumed standard model, admits a relative rank-two frame filling near its connecting interval.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalized_pair_frame_filling line 13