OAI/GroupTheory/SimpleAmenable/Simplicial/BarSegal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntervalBar.Diagram.outer_project line 15
2. lemma OAI.IntervalBar.Diagram.outer_project_ε line 16
3. lemma OAI.IntervalBar.Diagram.outer_project_μ line 20
4. instance OAI.IntervalBar.Diagram.outer_project_monoidal line 25
5. lemma OAI.IntervalBar.Diagram.barMap_congr line 36
6. lemma OAI.IntervalBar.Diagram.bar₂Map_congr line 43
7. lemma OAI.IntervalBar.Diagram.rows₂_segal line 55
8. lemma OAI.IntervalBar.Diagram.rows₃_segal line 66
9. lemma OAI.IntervalBar.Diagram.rows₂_segal_homology_isIso line 77
10. lemma OAI.IntervalBar.Diagram.rows₃_segal_homology_isIso line 85