OAI/GroupTheory/SimpleAmenable/Simplicial/CoefficientNerve.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CoefficientNerve.Simplex line 13
  2. abbrev OAI.CoefficientNerve.Coeff line 14
  3. abbrev OAI.CoefficientNerve.Obj line 15
  4. def OAI.CoefficientNerve.single line 16
  5. def OAI.CoefficientNerve.desc line 18
  6. lemma OAI.CoefficientNerve.single_desc line 20
  7. lemma OAI.CoefficientNerve.hom_ext line 25
  8. def OAI.CoefficientNerve.trunc line 31
  9. def OAI.CoefficientNerve.tail line 33
  10. def OAI.CoefficientNerve.map line 36
  11. lemma OAI.CoefficientNerve.single_map line 38
  12. lemma OAI.CoefficientNerve.trunc_id line 40
  13. lemma OAI.CoefficientNerve.tail_id line 41
  14. lemma OAI.CoefficientNerve.trunc_comp line 44
  15. lemma OAI.CoefficientNerve.tail_comp line 46
  16. lemma OAI.CoefficientNerve.map_id line 53
  17. lemma OAI.CoefficientNerve.map_comp line 56
  18. def OAI.CoefficientNerve.simplicial line 60
  19. def OAI.CoefficientNerve.complex line 65
  20. def OAI.CoefficientNerve.post line 67
  21. lemma OAI.CoefficientNerve.single_post line 74
  22. lemma OAI.CoefficientNerve.post_id line 77
  23. lemma OAI.CoefficientNerve.post_comp line 85
  24. def OAI.NervePrefix.extra line 103
  25. lemma OAI.NervePrefix.zero line 105
  26. lemma OAI.NervePrefix.obj_zero line 106
  27. lemma OAI.NervePrefix.succ_obj line 107
  28. lemma OAI.NervePrefix.precomp_delta line 109