OAI/GroupTheory/UniversalGroup/TowerCoverings.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. class OAI.UniversalFInfinity.TopologicalTower.EquivariantSystem line 26
2. instance OAI.UniversalFInfinity.TopologicalTower.limitMulAction line 31
3. lemma OAI.UniversalFInfinity.TopologicalTower.smul_of line 43
4. instance OAI.UniversalFInfinity.TopologicalTower.(instance at line 46) line 46
5. def OAI.UniversalFInfinity.TopologicalTower.tailSet line 61
6. lemma OAI.UniversalFInfinity.TopologicalTower.preimage_tailSet line 64
7. lemma OAI.UniversalFInfinity.TopologicalTower.tailSet_isOpen line 87
8. structure OAI.UniversalFInfinity.TopologicalTower.Slice line 110
9. def OAI.UniversalFInfinity.TopologicalTower.ExtendsSlices line 115
10. def OAI.UniversalFInfinity.TopologicalTower.extendSlice line 120
11. lemma OAI.UniversalFInfinity.TopologicalTower.extendSlice_spec line 123
12. def OAI.UniversalFInfinity.TopologicalTower.sliceFamily line 127
13. lemma OAI.UniversalFInfinity.TopologicalTower.sliceFamily_self line 131
14. lemma OAI.UniversalFInfinity.TopologicalTower.sliceFamily_compat line 135
15. lemma OAI.UniversalFInfinity.TopologicalTower.tailSet_disjoint line 153
16. lemma OAI.UniversalFInfinity.TopologicalTower.exists_disjoint_nhds line 173
17. def OAI.UniversalFInfinity.TopologicalTower.limitMap line 206
18. lemma OAI.UniversalFInfinity.TopologicalTower.limitMap_of line 211
19. lemma OAI.UniversalFInfinity.TopologicalTower.limitMap_isQuotient line 215
20. lemma OAI.UniversalFInfinity.TopologicalTower.limitMap_fibers line 235
21. lemma OAI.UniversalFInfinity.TopologicalTower.limitMap_isQuotientCovering line 254
22. lemma OAI.UniversalFInfinity.TopologicalTower.compactMap_factors line 274
23. def OAI.UniversalFInfinity.TopologicalTower.EventuallyFills line 287
24. lemma OAI.UniversalFInfinity.TopologicalTower.sphereFillable line 292
25. lemma OAI.UniversalFInfinity.TopologicalTower.contractible line 303