Skip to content

Commit f8ffcfb

Browse files
committed
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.
1 parent 7a175e0 commit f8ffcfb

File tree

4 files changed

+534
-502
lines changed

4 files changed

+534
-502
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4347,6 +4347,7 @@ import Mathlib.Topology.Compactness.PseudometrizableLindelof
43474347
import Mathlib.Topology.Compactness.SigmaCompact
43484348
import Mathlib.Topology.CompletelyRegular
43494349
import Mathlib.Topology.Connected.Basic
4350+
import Mathlib.Topology.Connected.Clopen
43504351
import Mathlib.Topology.Connected.LocallyConnected
43514352
import Mathlib.Topology.Connected.PathConnected
43524353
import Mathlib.Topology.Connected.Separation

0 commit comments

Comments
 (0)