Theorem OpenEmbedding.locPathConnectedSpace

Modification history

2024-10-18 21:29
Mathlib/Topology/Connected/PathConnected.lean
chore: Rename `OpenEmbedding` to `IsOpenEmbedding` (#17898) …
Deleted OpenEmbedding.locPathConnectedSpaceView on Github →
2024-10-18 05:56
Mathlib/Topology/Connected/PathConnected.lean
feat(PathConnected): review API, add missing lemmas (#17855)
Added OpenEmbedding.locPathConnectedSpaceView on Github →