OAI/GroupTheory/SimpleAmenable/Simplicial/RestrictedTripleDegree.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RestrictedNerve.property₂ line 16
2. abbrev OAI.RestrictedNerve.property₃ line 17
3. abbrev OAI.RestrictedNerve.pos₂ line 18
4. abbrev OAI.RestrictedNerve.pos₃ line 19
5. def OAI.RestrictedNerve.tripleTranspose line 20
6. instance OAI.RestrictedNerve.tripleTransposeEquivalence line 26
7. def OAI.RestrictedNerve.triplePosInclusion line 29
8. instance OAI.RestrictedNerve.triplePosInclusionEquivalence line 34
9. def OAI.RestrictedNerve.tripleDiagramHorizontal line 36
10. def OAI.RestrictedNerve.triplePosHomologyIso line 43
11. def OAI.RestrictedNerve.tripleTransposeHomologyIso line 48
12. def OAI.RestrictedNerve.tripleRestrictedHomologyIso line 53