Revision #2964 → #3484 · back to history
modifiedFactorisation of coverings (first)85b18570aaa1
| Field | From #2964 | To #3484 |
|---|
| note | No composition lemma for `IsCoveringMap` exists; `IsCoveringMap.comp` is absent. | No composition lemma for `IsCoveringMap` exists; `IsCoveringMap.comp` is absent (only `comp_homeomorph` for a homeomorphism factor). |
modifiedProduct of coverings is a covering618bd3604fef
| Field | From #2964 | To #3484 |
|---|
| note | No `Prod`-style lemma about `IsCoveringMap` exists in Mathlib. | No `Prod`-style lemma about `IsCoveringMap` exists in Mathlib (loogle finds no `IsCoveringMap.prod`). |