OAI/GroupTheory/FiniteType/RelativeChains.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RelativeChains.map_id line 13
  2. lemma OAI.RelativeChains.map_comp line 20
  3. lemma OAI.RelativeChains.homeomorph_quasiIso line 29
  4. lemma OAI.RelativeChains.excision_map_quasiIso line 39
  5. lemma OAI.RelativeChains.enlarge_quasiIso line 68
  6. abbrev OAI.CWExtension.Disk line 85
  7. abbrev OAI.CWExtension.Boundary line 86
  8. def OAI.CWExtension.charMap line 88
  9. theorem OAI.CWExtension.isClosed_of_cells line 93
  10. theorem OAI.CWExtension.continuous_of_cells line 120
  11. abbrev OAI.CWExtension.Skel line 134
  12. def OAI.CWExtension.skelIncl line 137
  13. def OAI.CWExtension.charSkel line 141
  14. def OAI.CWExtension.boundarySkel line 146
  15. def OAI.CWExtension.stageQuot line 152
  16. theorem OAI.CWExtension.stageQuot_surjective line 156
  17. theorem OAI.CWExtension.stageQuot_isQuotientMap line 166
  18. theorem OAI.CWExtension.boundary_of_mem_skel line 192
  19. def OAI.CWExtension.stageData line 201
  20. theorem OAI.CWExtension.stageData_factors line 207
  21. def OAI.CWExtension.extendSkel line 258
  22. theorem OAI.CWExtension.extendSkel_prior line 264
  23. theorem OAI.CWExtension.extendSkel_disk line 270