OAI/Topology/Homotopy/OpenCollapse.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Continuous collapse to a one-point compactification and parameterized descent.

  1. def OAI.NearbyLagrangian.OpenCollapse.collapse line 15
  2. lemma OAI.NearbyLagrangian.OpenCollapse.collapse_of_mem line 18
  3. lemma OAI.NearbyLagrangian.OpenCollapse.collapse_of_notMem line 20
  4. lemma OAI.NearbyLagrangian.OpenCollapse.collapse_eq_infty line 22
  5. lemma OAI.NearbyLagrangian.OpenCollapse.collapse_eq line 24
  6. lemma OAI.NearbyLagrangian.OpenCollapse.continuous_collapse line 38
  7. lemma OAI.NearbyLagrangian.OpenCollapse.collapse_surjective line 60
  8. lemma OAI.NearbyLagrangian.OpenCollapse.isQuotientMap_collapse line 67
  9. def OAI.NearbyLagrangian.OpenCollapse.descend line 73
  10. lemma OAI.NearbyLagrangian.OpenCollapse.descend_collapse line 86
  11. lemma OAI.NearbyLagrangian.OpenCollapse.continuous_descend_param line 104