OAI/GroupTheory/SimpleAmenable/Simplicial/LowerBarComposition.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntervalBar.Diagram.barMap_comp line 15
  2. lemma OAI.IntervalBar.Diagram.bar₂Map_comp line 20
  3. def OAI.BarFinitePower.powerTwoIso line 26
  4. def OAI.BarFinitePower.powerOneIso line 33
  5. abbrev OAI.SimplicialFirstFinite.K line 51
  6. def OAI.SimplicialFirstFinite.outer line 52
  7. def OAI.SimplicialFirstFinite.sec line 54
  8. lemma OAI.SimplicialFirstFinite.sigma_zero_two line 59
  9. lemma OAI.SimplicialFirstFinite.sigma_one_zero line 63
  10. lemma OAI.SimplicialFirstFinite.outer_sec line 67
  11. lemma OAI.SimplicialFirstFinite.d21 line 82
  12. lemma OAI.SimplicialFirstFinite.d10 line 84
  13. lemma OAI.SimplicialFirstFinite.sigma_d21 line 85
  14. lemma OAI.SimplicialFirstFinite.boundary_sec line 93
  15. lemma OAI.SimplicialFirstFinite.boundary_finite line 102
  16. lemma OAI.SimplicialFirstFinite.finite_one line 116
  17. def OAI.SimplicialDiagonal.segalTwo line 136
  18. def OAI.SimplicialDiagonal.segalKernelMap line 138
  19. lemma OAI.SimplicialDiagonal.segalKernelMap_injective line 156
  20. lemma OAI.SimplicialDiagonal.outer_kernel_finite line 161