OAI/Topology/ArtinGroups/Harmonic/OrderMappingCylinder.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.OrderMappingCylinder line 13
2. def OAI.HarmonicArtin.OrderMappingCylinder.le line 18
3. instance OAI.HarmonicArtin.OrderMappingCylinder.(instance at line 24) line 24
4. def OAI.HarmonicArtin.OrderMappingCylinder.left line 59
5. def OAI.HarmonicArtin.OrderMappingCylinder.right line 60
6. def OAI.HarmonicArtin.OrderMappingCylinder.project line 61
7. lemma OAI.HarmonicArtin.OrderMappingCylinder.project_right line 73
8. lemma OAI.HarmonicArtin.OrderMappingCylinder.le_right_project line 74
9. def OAI.HarmonicArtin.OrderMappingCylinder.nerveEquiv line 77
10. lemma OAI.HarmonicArtin.OrderMappingCylinder.weights_contractible line 81
11. def OAI.HarmonicArtin.OrderMappingCylinder.old line 86
12. def OAI.HarmonicArtin.OrderMappingCylinder.oldIso line 88
13. lemma OAI.HarmonicArtin.OrderMappingCylinder.not_old_iff line 95
14. def OAI.HarmonicArtin.OrderMappingCylinder.rank line 106
15. lemma OAI.HarmonicArtin.OrderMappingCylinder.rank_bound line 110
16. lemma OAI.HarmonicArtin.OrderMappingCylinder.rank_strict line 116
17. def OAI.HarmonicArtin.OrderMappingCylinder.oldLowerIso line 128