OAI/GroupTheory/UniversalGroup/CellularApproximation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniversalFInfinity.Cellular.skeletonBoundary line 24
2. def OAI.UniversalFInfinity.Cellular.skeletonBase line 29
3. def OAI.UniversalFInfinity.Cellular.skeletonCell line 32
4. def OAI.UniversalFInfinity.Cellular.skeletonAssembly line 37
5. lemma OAI.UniversalFInfinity.Cellular.skeletonAssembly_base line 40
6. lemma OAI.UniversalFInfinity.Cellular.skeletonAssembly_cell line 44
7. lemma OAI.UniversalFInfinity.Cellular.skeletonAssembly_interior line 48
8. lemma OAI.UniversalFInfinity.Cellular.skeletonAssembly_injective line 52
9. lemma OAI.UniversalFInfinity.Cellular.skeletonAssembly_surjective line 82
10. lemma OAI.UniversalFInfinity.Cellular.skeletonAssembly_closed line 97
11. def OAI.UniversalFInfinity.Cellular.skeletonHomeomorph line 142
12. lemma OAI.UniversalFInfinity.Cellular.skeleton_smul_mem line 161
13. def OAI.UniversalFInfinity.Cellular.skeletonTranslate line 171
14. lemma OAI.UniversalFInfinity.Cellular.skeletonTranslate_base line 175
15. lemma OAI.UniversalFInfinity.Cellular.skeletonTranslate_cell line 179
16. lemma OAI.UniversalFInfinity.Cellular.exists_equivariant_skeleton_extension line 187
17. lemma OAI.UniversalFInfinity.Cellular.exists_equivariant_skeleton_lift line 253
18. lemma OAI.UniversalFInfinity.Cellular.isEmpty_skeleton_zero line 340
19. lemma OAI.UniversalFInfinity.Cellular.exists_equivariant_lift_on_skeleton line 350
20. lemma OAI.UniversalFInfinity.Cellular.exists_equivariant_map_on_skeleton line 367
21. lemma OAI.UniversalFInfinity.Cellular.exists_equivariant_homotopy_on_skeleton line 381
22. def OAI.UniversalFInfinity.Cellular.skeletonChart line 402
23. lemma OAI.UniversalFInfinity.Cellular.skeleton_compact_representatives line 407
24. def OAI.UniversalFInfinity.Cellular.skeletonInclusion line 432
25. lemma OAI.UniversalFInfinity.Cellular.deform_skeleton_succ line 434
26. lemma OAI.UniversalFInfinity.Cellular.deform_bounded_skeleton line 460
27. theorem OAI.UniversalFInfinity.Cellular.exists_cellular_approximation line 496
28. lemma OAI.UniversalFInfinity.SphereTopology.fill_zero line 508
29. lemma OAI.UniversalFInfinity.SphereTopology.fill_one line 516
30. lemma OAI.UniversalFInfinity.Milnor.controlled_skeleton_homotopy line 542
31. lemma OAI.UniversalFInfinity.Milnor.uniform_low_connectivity line 563