Theorem Homeomorph.preimage_pathComponent

Modification history

2026-08-13 15:21
Mathlib/Topology/Connected/PathConnected.lean
feat(Topology/Connected): transport path-connectedness along homeomorphisms (#41665) …
Added Homeomorph.preimage_pathComponentView on Github →