OAI/Topology/ArtinGroups/Realizations/CellUnion.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.SourceCellUnion line 13
2. inductive OAI.HarmonicArtin.SourceFaceIdentification line 15
3. abbrev OAI.HarmonicArtin.SourceGluingRelation line 20
4. def OAI.HarmonicArtin.SourceSalvetti line 22
5. instance OAI.HarmonicArtin.(instance at line 24) line 24
6. def OAI.HarmonicArtin.sourceUnionMap line 27
7. lemma OAI.HarmonicArtin.sourceCellMap_normal line 32
8. lemma OAI.HarmonicArtin.sourceUnionMap_lifted line 39
9. lemma OAI.HarmonicArtin.sourceGluing_face_le line 44
10. lemma OAI.HarmonicArtin.sourceUnionMap_rel line 53
11. lemma OAI.HarmonicArtin.sourceUnionMap_kernel line 67
12. lemma OAI.HarmonicArtin.sourceUnionMap_surjective line 99
13. lemma OAI.HarmonicArtin.sourceUnionMap_quotient line 106
14. def OAI.HarmonicArtin.sourceSalvettiToDeck line 125
15. lemma OAI.HarmonicArtin.sourceSalvettiToDeck_bijective line 129
16. lemma OAI.HarmonicArtin.sourceSalvettiToDeck_quotient line 140
17. def OAI.HarmonicArtin.sourceSalvettiHomeomorph line 144
18. def OAI.HarmonicArtin.sourceUniversalProjection line 153
19. theorem OAI.HarmonicArtin.sourceUniversalProjection_quotientCovering line 156
20. theorem OAI.HarmonicArtin.source_full_cover_contractible line 160