Commit 2021-02-16 09:30 2961e79c
View on Github →feat(topology/connected.lean): define pi_0 and prove basic properties (#6188)
Define and prove basic properties of pi_0, the functor quotienting a space by its connected components.
For dot notation convenience, this PR renames subset_connected_component
to is_preconnected.subset_connected_component
and also defines the weaker version is_connected.subset_connected_component
.