Commit 2023-10-18 21:09 51c79693

View on Github →

feat: split Topology/Connected.lean (#7646) In the last step, I have removed redundant imports: those which are implied by the other imports. I can revert those changes if desired/if this seems too brittle.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

Modified Mathlib/Analysis/Convex/Topology.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Renamed Mathlib/Topology/Connected.lean to Mathlib/Topology/Connected/Basic.lean

deleted def Continuous.connectedComponentsLift

deleted theorem Continuous.connectedComponentsLift_apply_coe

deleted theorem Continuous.connectedComponentsLift_comp_coe

deleted theorem Continuous.connectedComponentsLift_continuous

deleted theorem Continuous.connectedComponentsLift_unique

deleted def Continuous.connectedComponentsMap

deleted theorem Continuous.connectedComponentsMap_continuous

deleted theorem Continuous.image_connectedComponent_eq_singleton

deleted theorem Continuous.image_eq_of_connectedComponent_eq

deleted theorem Embedding.isTotallyDisconnected

deleted theorem IsOpen.locallyConnectedSpace

deleted theorem IsPreconnected.constant

deleted theorem IsPreconnected.constant_of_mapsTo

deleted theorem IsPreconnected.eqOn_const_of_mapsTo

deleted theorem IsPreconnected.subsingleton

deleted def IsTotallyDisconnected

deleted def IsTotallySeparated

deleted theorem OpenEmbedding.locallyConnectedSpace

deleted theorem PreconnectedSpace.constant

deleted theorem connectedComponentIn_mem_nhds

deleted theorem connectedComponent_eq_singleton

deleted theorem connectedComponents_lift_unique'

deleted theorem exists_clopen_of_totally_separated

deleted theorem isClopen_connectedComponent

deleted theorem isOpen_connectedComponent

deleted theorem isTotallyDisconnected_empty

deleted theorem isTotallyDisconnected_of_clopen_set

deleted theorem isTotallyDisconnected_of_image

deleted theorem isTotallyDisconnected_of_isTotallySeparated

deleted theorem isTotallyDisconnected_of_totallyDisconnectedSpace

deleted theorem isTotallyDisconnected_singleton

deleted theorem isTotallySeparated_empty

deleted theorem isTotallySeparated_singleton

deleted theorem locallyConnectedSpace_iff_connectedComponentIn_open

deleted theorem locallyConnectedSpace_iff_connected_basis

deleted theorem locallyConnectedSpace_iff_connected_subsets

deleted theorem locallyConnectedSpace_iff_open_connected_basis

deleted theorem locallyConnectedSpace_iff_open_connected_subsets

deleted theorem locallyConnectedSpace_of_connected_bases

deleted theorem totallyDisconnectedSpace_iff_connectedComponent_singleton

deleted theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton

Created Mathlib/Topology/Connected/LocallyConnected.lean

added theorem IsOpen.locallyConnectedSpace

added theorem OpenEmbedding.locallyConnectedSpace

added theorem connectedComponentIn_mem_nhds

added theorem isClopen_connectedComponent

added theorem isOpen_connectedComponent

added theorem locallyConnectedSpace_iff_connectedComponentIn_open

added theorem locallyConnectedSpace_iff_connected_basis

added theorem locallyConnectedSpace_iff_connected_subsets

added theorem locallyConnectedSpace_iff_open_connected_basis

added theorem locallyConnectedSpace_iff_open_connected_subsets

added theorem locallyConnectedSpace_of_connected_bases

Renamed Mathlib/Topology/PathConnected.lean to Mathlib/Topology/Connected/PathConnected.lean

Created Mathlib/Topology/Connected/TotallyDisconnected.lean

added def Continuous.connectedComponentsLift

added theorem Continuous.connectedComponentsLift_apply_coe

added theorem Continuous.connectedComponentsLift_comp_coe

added theorem Continuous.connectedComponentsLift_continuous

added theorem Continuous.connectedComponentsLift_unique

added def Continuous.connectedComponentsMap

added theorem Continuous.connectedComponentsMap_continuous

added theorem Continuous.image_connectedComponent_eq_singleton

added theorem Continuous.image_eq_of_connectedComponent_eq

added theorem Embedding.isTotallyDisconnected

added theorem IsPreconnected.constant

added theorem IsPreconnected.constant_of_mapsTo

added theorem IsPreconnected.eqOn_const_of_mapsTo

added theorem IsPreconnected.subsingleton

added def IsTotallyDisconnected

added def IsTotallySeparated

added theorem PreconnectedSpace.constant

added theorem connectedComponent_eq_singleton

added theorem connectedComponents_lift_unique'

added theorem exists_clopen_of_totally_separated

added theorem isTotallyDisconnected_empty

added theorem isTotallyDisconnected_of_clopen_set

added theorem isTotallyDisconnected_of_image

added theorem isTotallyDisconnected_of_isTotallySeparated

added theorem isTotallyDisconnected_of_totallyDisconnectedSpace

added theorem isTotallyDisconnected_singleton

added theorem isTotallySeparated_empty

added theorem isTotallySeparated_singleton

added theorem totallyDisconnectedSpace_iff_connectedComponent_singleton

added theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton

Modified Mathlib/Topology/ContinuousFunction/Sigma.lean

Modified Mathlib/Topology/Homotopy/Path.lean

Modified Mathlib/Topology/Instances/AddCircle.lean

Modified Mathlib/Topology/LocallyConstant/Basic.lean

Modified Mathlib/Topology/Separation.lean