OAI/GroupTheory/SimpleAmenable/Simplicial/RestrictedFunctorial.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RestrictedNerve.stringsMap line 16
  2. def OAI.RestrictedNerve.verticalMap line 21
  3. def OAI.RestrictedNerve.horizontalMap line 26
  4. def OAI.RestrictedNerve.verticalMapNat line 34
  5. lemma OAI.RestrictedNerve.diagonalIso_natural line 42
  6. lemma OAI.RestrictedNerve.eqToHom_vertical_app line 51
  7. lemma OAI.RestrictedNerve.constantMap_natural line 54
  8. lemma OAI.RestrictedNerve.constantDiagonalIso_natural line 77
  9. lemma OAI.RestrictedNerve.homologyIso_natural line 88
  10. def OAI.RestrictedNerve.posReindex line 133
  11. lemma OAI.RestrictedNerve.posReindex_property line 139
  12. lemma OAI.RestrictedNerve.posReindex_inclusion line 142
  13. lemma OAI.RestrictedNerve.posReindex_id line 149
  14. lemma OAI.RestrictedNerve.posReindex_comp line 155
  15. lemma OAI.RestrictedNerve.transpose_posReindex line 161