OAI/GroupTheory/SimpleAmenable/Homology/TotalSingle.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TotalHomotopy.equiv line 15
  2. abbrev OAI.TotalHomotopy.single line 22
  3. def OAI.TotalHomotopy.singleIn line 24
  4. def OAI.TotalHomotopy.singleOutF line 31
  5. lemma OAI.TotalHomotopy.singleIn_out line 39
  6. lemma OAI.TotalHomotopy.singleOut_in line 44
  7. instance OAI.TotalHomotopy.singleIn_isIso line 60
  8. def OAI.TotalHomotopy.singleIso line 65
  9. abbrev OAI.BiResolution.c line 79
  10. def OAI.BiResolution.pointAugmentation line 81
  11. def OAI.BiResolution.pointAugmented line 85
  12. def OAI.BiResolution.pointExtra line 90
  13. def OAI.BiResolution.complexAt line 115
  14. def OAI.BiResolution.complexAtIso line 118
  15. def OAI.BiResolution.complexAtEquiv line 124
  16. def OAI.BiResolution.totalAtEquiv line 131
  17. abbrev OAI.TotalFunctor.map₂ line 148
  18. def OAI.TotalFunctor.comparisonF line 151
  19. lemma OAI.TotalFunctor.ι_comparisonF line 155
  20. def OAI.TotalFunctor.comparison line 160
  21. instance OAI.TotalFunctor.comparisonF_isIso line 194
  22. instance OAI.TotalFunctor.comparison_isIso line 199
  23. def OAI.TotalFunctor.iso line 204