OAI/GroupTheory/SimpleAmenable/Simplicial/CoefficientFiltered.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoefficientNerve.single_eq line 14
2. def OAI.CoefficientNerve.overLift line 18
3. lemma OAI.CoefficientNerve.overLift_forget line 27
4. lemma OAI.CoefficientNerve.overLift_map line 33
5. def OAI.CoefficientNerve.overDiagram line 48
6. def OAI.CoefficientNerve.overCocone line 67
7. def OAI.CoefficientNerve.overPointwiseIsColimit line 77
8. def OAI.CoefficientNerve.overIsColimit line 106
9. instance OAI.CoefficientNerve.alternating_preserves line 114
10. lemma OAI.CoefficientNerve.positive_acyclic line 121