Theorem Topology.IsCoinducing.isConnected_preimage_of_isClosed

Modification history

2026-04-07 17:44
Mathlib/Topology/Connected/Clopen.lean
chore(Topology/Connected): generalize `preimage_connectedComponent_connected` to closed connected sets (#37514)
Added Topology.IsCoinducing.isConnected_preimage_of_isClosedView on Github →