Commit 2026-04-07 17:44 632b417a

View on Github →

chore(Topology/Connected): generalize preimage_connectedComponent_connected to closed connected sets (#37514)

Estimated changes

Modified Mathlib/Topology/Connected/Clopen.lean

added theorem Topology.IsCoinducing.isConnected_preimage_of_isClosed

modified theorem preimage_connectedComponent_connected