Commit 2025-04-03 15:25 4e861397

View on Github →

chore(Topology): improve API and golf (#23633) Deprecate isTotallyDisconnected_of_isClopen_set because it encourages people to prove the weaker TotallyDisconnectedSpace rather than the stronger TotallySeparatedSpace. Prove IsTopologicalBasis.of_isOpen_of_subset and use it to golf IsTopologicalBasis.insert_empty and PrespectralSpace.of_isTopologicalBasis.

Estimated changes

Modified Mathlib/FieldTheory/KrullTopology.lean

added theorem krullTopology_isTotallySeparated

deleted theorem krullTopology_totallyDisconnected

Modified Mathlib/Topology/Bases.lean

added theorem TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

Modified Mathlib/Topology/Spectral/Prespectral.lean