Commit 2025-04-09 06:49 b8b5d195

View on Github →

chore(Topology/Separation): split connectedness out of basic file (#23827)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

Modified Mathlib/Topology/Algebra/ClopenNhdofOne.lean

Modified Mathlib/Topology/Connected/Separation.lean

Modified Mathlib/Topology/DiscreteQuotient.lean

Modified Mathlib/Topology/DiscreteSubset.lean

Modified Mathlib/Topology/Homeomorph/Lemmas.lean

Modified Mathlib/Topology/Order/IntermediateValue.lean

Modified Mathlib/Topology/Order/Priestley.lean

Modified Mathlib/Topology/SeparatedMap.lean

Modified Mathlib/Topology/Separation/Basic.lean

deleted theorem IsPreconnected.infinite_of_nontrivial

deleted theorem PreconnectedSpace.infinite

deleted theorem PreconnectedSpace.trivial_of_discrete

Created Mathlib/Topology/Separation/Connected.lean

added theorem IsPreconnected.infinite_of_nontrivial

added theorem PreconnectedSpace.infinite

added theorem PreconnectedSpace.trivial_of_discrete

Modified Mathlib/Topology/Separation/Hausdorff.lean

Modified Mathlib/Topology/Separation/Profinite.lean

Modified Mathlib/Topology/Separation/Regular.lean

Modified Mathlib/Topology/Sets/Closeds.lean

Modified Mathlib/Topology/StoneCech.lean

Modified scripts/noshake.json