[Merged by Bors] - feat(Topology): An open cover of a preconnected set has no isolated components#39691

Raph-DG wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

Raph-DG:Raph-DG-TransGenRaph-DG/mathlib4:Raph-DG-TransGenCopy head branch name to clipboard