OAI/GroupTheory/FiniteType/DiskSigmaCollar.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DiskSigmaCollar.Disks line 15
  2. abbrev OAI.DiskSigmaCollar.Opens line 16
  3. def OAI.DiskSigmaCollar.radius line 18
  4. def OAI.DiskSigmaCollar.boundary line 20
  5. def OAI.DiskSigmaCollar.collar line 21
  6. lemma OAI.DiskSigmaCollar.boundary_closed line 22
  7. lemma OAI.DiskSigmaCollar.collar_open line 23
  8. lemma OAI.DiskSigmaCollar.boundary_subset_collar line 24
  9. def OAI.DiskSigmaCollar.paths line 28
  10. lemma OAI.DiskSigmaCollar.paths_zero line 34
  11. lemma OAI.DiskSigmaCollar.paths_mem line 35
  12. lemma OAI.DiskSigmaCollar.paths_one line 37
  13. lemma OAI.DiskSigmaCollar.paths_fixed line 41
  14. def OAI.DiskSigmaCollar.inclusion line 46
  15. def OAI.DiskSigmaCollar.retract line 48
  16. def OAI.DiskSigmaCollar.homotopy line 51
  17. def OAI.DiskSigmaCollar.collarEquiv line 57
  18. def OAI.DiskSigmaCollar.openMap line 70
  19. lemma OAI.DiskSigmaCollar.openMap_embedding line 71
  20. lemma OAI.DiskSigmaCollar.openMap_mem line 74
  21. lemma OAI.DiskSigmaCollar.openMap_surj line 77
  22. def OAI.DiskSigmaCollar.openEquiv line 84
  23. lemma OAI.DiskSigmaCollar.openEquiv_apply line 87
  24. abbrev OAI.CWSingularPair.Disks line 95
  25. abbrev OAI.CWSingularPair.Boundary line 96
  26. abbrev OAI.CWSingularPair.Collar line 97
  27. def OAI.CWSingularPair.attach line 99
  28. lemma OAI.CWSingularPair.radius_attach line 102
  29. lemma OAI.CWSingularPair.maps_boundary line 106
  30. lemma OAI.CWSingularPair.maps_collar line 111
  31. def OAI.CWSingularPair.complementEquiv line 117
  32. lemma OAI.CWSingularPair.complementEquiv_apply line 120
  33. lemma OAI.CWSingularPair.collar_map_quasiIso line 128
  34. theorem OAI.CWSingularPair.quasiIso line 141
  35. def OAI.RelativeChains.quotientMap line 170
  36. lemma OAI.RelativeChains.quotientMap_projection line 173
  37. def OAI.RelativeChains.triple line 178
  38. lemma OAI.RelativeChains.triple_shortExact line 187
  39. lemma OAI.RelativeChains.univ_isZero line 208
  40. lemma OAI.SingularChains.constant_quasiIso line 223