OAI/Geometry/NearbyLagrangian/MainReduction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Class persistence and the conditional reduction to the two topological hypotheses.

  1. theorem OAI.NearbyLagrangian.Tubes.localized_analytic_obstruction line 18
  2. theorem OAI.NearbyLagrangian.Tubes.HasRestoredEndpoint.class_persistence line 36
  3. def OAI.NearbyLagrangian.Tubes.OneCriticalTubeNullityGoal line 66
  4. theorem OAI.NearbyLagrangian.main_reduction line 87