TranslationCovering.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A covering from two-sided translation coordinates

A local group parameterization whose left and right translations are global homeomorphisms is a covering map. No associativity on the parameter space is needed for this step.

theorem OAI.PolycyclicRecognition.kernel_discrete line 29
theorem OAI.PolycyclicRecognition.right_inverse_fiber line 40
def OAI.PolycyclicRecognition.translationFiberHomeomorph line 49
theorem OAI.PolycyclicRecognition.evenlyCovered_one_of_translations line 82
theorem OAI.PolycyclicRecognition.covering_of_translations line 93
def OAI.PolycyclicRecognition.homeomorphOfSimplyConnectedCovering line 110
Source documentation
A covering of a simply connected space from a connected space has a continuous global inverse.
```
def homeomorphOfSimplyConnectedCovering [PreconnectedSpace V]
    [SimplyConnectedSpace G] [LocallyPathConnectedSpace G]
    (cov : IsCoveringMap f) : V ≃ₜ G := by
…
```