OAI/GroupTheory/FiniteType/RegularCoverGeometry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RegularCoverGeometry.pathConnected_of_monodromy_transitive line 18
  2. theorem OAI.RegularCoverGeometry.simplyConnected_of_monodromy_bijective line 34
  3. def OAI.CoveringMapNatural.fiberMap line 60
  4. lemma OAI.CoveringMapNatural.natural line 63
  5. lemma OAI.CoveringMapNatural.monodromy_point_bijective line 78
  6. lemma OAI.CoveringMapNatural.fundamentalMap_injective line 98
  7. theorem OAI.CoveringMapNatural.simplyConnected_of_old line 109
  8. def OAI.FiberCoreMap.map line 152
  9. lemma OAI.FiberCoreMap.map_proj line 155
  10. lemma OAI.FiberCoreMap.map_chart line 158
  11. lemma OAI.FiberCoreMap.continuous_map line 166
  12. def OAI.FiberCoreMap.continuousMap line 182
  13. lemma OAI.FiberCoreMap.fiber_bijective line 185
  14. def OAI.PresentationGeometry.CellCoverExtension.oldLift line 211
  15. lemma OAI.PresentationGeometry.CellCoverExtension.oldLift_proj line 217
  16. lemma OAI.PresentationGeometry.CellCoverExtension.oldLift_fiber_bijective line 221
  17. theorem OAI.PresentationGeometry.CellCoverExtension.coveringCore_simplyConnected line 230
  18. lemma OAI.PresentationGeometry.CellCoverExtension.fundamentalGroupMap_bijective line 243