Commit 2024-07-26 00:02 f8ffcfb2

chore: split Topology.Connected.Basic (#15144) This splits Topology.Connected.Basic approximately in half, into Basic and Clopen. This removes the Mathlib.Topology.Clopen import from Basic, and allows for one more file import from #14927 in the Clopen file. As far as declaration order goes, only the first 5 results in Clopen were moved "down" into the Clopen file, and only the last 4 results in Basic were moved "up" into the Basic file. Otherwise no changes except for new module documentation were made.