OAI/GroupTheory/UniversalGroup/UniverseTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniversalFInfinity.UniverseTransport.transportedMap line 25
2. lemma OAI.UniversalFInfinity.UniverseTransport.transportedMap_apply line 28
3. lemma OAI.UniversalFInfinity.UniverseTransport.transportedMap_source line 31
4. lemma OAI.UniversalFInfinity.UniverseTransport.transportedMap_image line 37
5. lemma OAI.UniversalFInfinity.UniverseTransport.transportedMap_continuousOn line 41
6. lemma OAI.UniversalFInfinity.UniverseTransport.transportedMap_continuousOn_symm line 45
7. abbrev OAI.UniversalFInfinity.UniverseTransport.liftMap line 63
8. def OAI.UniversalFInfinity.UniverseTransport.liftCW line 67
9. def OAI.UniversalFInfinity.UniverseTransport.liftedCover line 128
10. lemma OAI.UniversalFInfinity.UniverseTransport.liftedCover_quotient line 130
11. theorem OAI.UniversalFInfinity.Brown.geometric_lifted_of_uniform line 160