OAI/GroupTheory/SimpleAmenable/Simplicial/RestrictedNerve.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.RestrictedNerve.(instance at line 10) line 10
  2. abbrev OAI.RestrictedNerve.Strings line 14
  3. def OAI.RestrictedNerve.allowed line 15
  4. abbrev OAI.RestrictedNerve.Vertical line 17
  5. def OAI.RestrictedNerve.reindex line 19
  6. lemma OAI.RestrictedNerve.reindex_id line 24
  7. lemma OAI.RestrictedNerve.reindex_comp line 29
  8. def OAI.RestrictedNerve.vreindex line 36
  9. lemma OAI.RestrictedNerve.vreindex_id line 42
  10. lemma OAI.RestrictedNerve.vreindex_comp line 48
  11. def OAI.RestrictedNerve.constant line 55
  12. def OAI.RestrictedNerve.evaluation line 58
  13. def OAI.RestrictedNerve.constantComparison line 61
  14. def OAI.RestrictedNerve.equivalence line 91
  15. instance OAI.RestrictedNerve.(instance at line 100) line 100
  16. def OAI.RestrictedNerve.horizontal line 103
  17. def OAI.RestrictedNerve.vertical line 108
  18. def OAI.RestrictedNerve.constantMap line 113
  19. def OAI.RestrictedNerve.transpose line 122
  20. def OAI.RestrictedNerve.untranspose line 135
  21. lemma OAI.RestrictedNerve.untranspose_transpose line 147
  22. lemma OAI.RestrictedNerve.transpose_untranspose line 155
  23. def OAI.RestrictedNerve.diagonalIso line 163
  24. def OAI.RestrictedNerve.constantDiagonalIso line 178
  25. def OAI.RestrictedNerve.homologyIso line 181