OAI/GroupTheory/FiniteType/CWCellular.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CWCellular.absolute line 14
  2. abbrev OAI.CWCellular.relative line 15
  3. def OAI.CWCellular.lowerHomeo line 17
  4. def OAI.CWCellular.lowerIso line 26
  5. def OAI.CWCellular.sequence line 30
  6. lemma OAI.CWCellular.sequence_f line 36
  7. def OAI.CWCellular.sequenceIso line 41
  8. lemma OAI.CWCellular.shortExact line 45
  9. lemma OAI.CWCellular.above line 48
  10. abbrev OAI.CWCellular.cell line 60
  11. def OAI.CWCellular.q line 62
  12. def OAI.CWCellular.delta line 65
  13. lemma OAI.CWCellular.q_mono line 68
  14. def OAI.CWCellular.d line 71
  15. lemma OAI.CWCellular.d_comp_d line 73
  16. def OAI.CWCellular.complex line 78
  17. lemma OAI.CWCellular.top_injective line 80
  18. lemma OAI.CWCellular.q_d line 84
  19. lemma OAI.CWCellular.top_image line 88
  20. def OAI.CWExtension.skelLE line 111
  21. def OAI.CWExtension.skelToComplex line 115
  22. def OAI.CWExtension.wholeQuot line 119
  23. theorem OAI.CWExtension.wholeQuot_surjective line 122
  24. theorem OAI.CWExtension.wholeQuot_isQuotientMap line 130
  25. theorem OAI.CWExtension.family_compat line 140
  26. def OAI.CWExtension.familyData line 148
  27. theorem OAI.CWExtension.familyData_factors line 151
  28. def OAI.CWExtension.unionMap line 161
  29. theorem OAI.CWExtension.unionMap_skel line 165
  30. lemma OAI.CWExtension.finite_subset_skel line 176
  31. lemma OAI.CWExtension.compact_subset_skel line 196