OAI/GroupTheory/SimpleAmenable/Simplicial/BarRowFiniteness.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BarFinitePower.singleRowComparison line 13
  2. lemma OAI.BarFinitePower.singleRowComparison_isIso line 16
  3. def OAI.BarFinitePower.doubleRowComparison line 22
  4. lemma OAI.BarFinitePower.doubleRowComparison_isIso line 25
  5. lemma OAI.BarFinitePower.singleRow_finite line 31
  6. lemma OAI.BarFinitePower.doubleRow_finite line 37
  7. def OAI.BarFinitePower.firstRowHomologyIso line 43
  8. def OAI.BarFinitePower.firstDoubleRowHomologyIso line 48
  9. lemma OAI.IntervalBar.Diagram.bar₂_finite_reverse line 63
  10. lemma OAI.IntervalBar.Diagram.bar₃_finite_reverse line 75
  11. lemma OAI.IntervalBar.Diagram.bar_finite_of_triple line 90
  12. def OAI.NerveComponents.toSkeletonπ line 104
  13. def OAI.NerveComponents.fromSkeletonπ line 106
  14. lemma OAI.NerveComponents.roundtrip line 108
  15. def OAI.NerveComponents.componentEquiv line 113
  16. def OAI.NerveComponents.map line 118
  17. lemma OAI.NerveComponents.map_mk line 120
  18. lemma OAI.NerveComponents.naturality line 121
  19. def OAI.NerveComponents.zeroIso line 125
  20. def OAI.NerveComponents.vertex line 127
  21. lemma OAI.NerveComponents.vertex_zeroIso line 130
  22. lemma OAI.NerveComponents.vertex_natural line 141
  23. lemma OAI.NerveComponents.hom_ext line 149
  24. lemma OAI.NerveComponents.zeroIso_natural line 164