OAI/Geometry/SurfaceImmersion/Atlas/CoordinateSardThree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact three-dimensional coordinate Sard and regular-fiber facts needed for generic projections of a surface from four-space to three-space.

  1. abbrev OAI.ClosedSurfaceR4.PublishedInputs.SurfaceDirectionParameters line 13
  2. theorem OAI.ClosedSurfaceR4.PublishedInputs.smooth_coordinate_critical_values_null line 15
  3. lemma OAI.ClosedSurfaceR4.PublishedInputs.regular_coordinate_point_locally_injective line 51
  4. theorem OAI.ClosedSurfaceR4.PublishedInputs.finite_compact_coordinate_regular_fiber line 70