OAI/GroupTheory/SimpleAmenable/Simplicial/TrajectoryFinite.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimplicialDiagonal.rowsIso line 13
2. def OAI.SimplicialDiagonal.homologyRowIso line 18
3. def OAI.SimplicialDiagonal.homologyRowHomologyIso line 23
4. lemma OAI.SimplicialDiagonal.rows_connected line 27
5. lemma OAI.BarHomology.zeroRow_finite line 35
6. lemma OAI.RestrictedNerve.stringBarRows_connected line 52
7. lemma OAI.RestrictedNerve.finite_bar₃_of_string line 54
8. def OAI.SimpleAmenable.PolygonObject.LabelledStage.trajectoryE2Iso line 63
9. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.trajectoryE2_finite line 71
10. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.polygon_bar₃_finite_of_symmetric line 83
11. lemma OAI.SimplicialDiagonal.finite_reverse_step line 111
12. lemma OAI.SimplicialDiagonal.finite_reverse line 135