Revision #1113 → #2546 · back to history
modifiedLocally path-connected implies locally connected888318ea13fd
| Field | From #1113 | To #2546 |
|---|
| mathlib.decl | LocPathConnectedSpace.toLocallyConnectedSpace | instLocallyConnectedSpace |
| provenance | ai | ai-moderated |
modifiedProduct of connected spaces is connected6a87d21b6d0c
| Field | From #1113 | To #2546 |
|---|
| mathlib.decl | Pi.connectedSpace | instConnectedSpaceForall |
| provenance | ai | ai-moderated |
modifiedContractible implies path connected71afa4b08c6a
| Field | From #1113 | To #2546 |
|---|
| mathlib.decl | ContractibleSpace.toPathConnectedSpace | ContractibleSpace.instPathConnectedSpace |
| provenance | ai | ai-moderated |