OAI/GroupTheory/UniversalGroup/CellularChains.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniversalFInfinity.Cellular.exists_equivariant_skeleton_extension_cells line 31
2. def OAI.UniversalFInfinity.Cellular.skeletonObstructions line 97
3. abbrev OAI.UniversalFInfinity.Cellular.SkeletonAttachment line 100
4. def OAI.UniversalFInfinity.Cellular.attachmentBase line 103
5. theorem OAI.UniversalFInfinity.Cellular.extend_by_cell_orbits line 108
6. lemma OAI.UniversalFInfinity.Cellular.exists_equivariant_skeleton_lift_cells line 140
7. lemma OAI.UniversalFInfinity.Cellular.cylinder_filling_from_disk line 218
8. lemma OAI.UniversalFInfinity.Attachment.representative_filling line 269
9. def OAI.UniversalFInfinity.Cellular.homotopyObstructions line 294
10. abbrev OAI.UniversalFInfinity.Cellular.HomotopyAttachment line 299
11. def OAI.UniversalFInfinity.Cellular.homotopyAttachmentBase line 302
12. theorem OAI.UniversalFInfinity.Cellular.homotopy_extend_by_cell_orbits line 305
13. lemma OAI.UniversalFInfinity.Cellular.exists_equivariant_skeleton_lift_cells_pred line 349
14. def OAI.UniversalFInfinity.Cellular.pathZero line 439
15. def OAI.UniversalFInfinity.Cellular.pathOne line 440
16. def OAI.UniversalFInfinity.Cellular.pathEvaluation line 442
17. def OAI.UniversalFInfinity.Cellular.pausePaths line 448
18. lemma OAI.UniversalFInfinity.Cellular.pausePaths_zero line 452
19. lemma OAI.UniversalFInfinity.Cellular.pausePaths_one line 454
20. lemma OAI.UniversalFInfinity.Cellular.pausePaths_smul line 457
21. lemma OAI.UniversalFInfinity.Cellular.dimH_disk_le line 467
22. lemma OAI.UniversalFInfinity.Cellular.disk_homotopy_into_skeleton line 472