OAI/Geometry/SurfaceImmersion/Atlas/PairChartSard.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The precise one-excess-dimension Sard instances for global double curves: three to two, then four to three.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.three_two_critical_values_null line 13
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.three_two_local_critical_values_null line 23
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pair_chart_critical_values_null line 28
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pair_chart_local_critical_values_null line 40