Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

Modified src/topology/connected.lean

added theorem connected_component_disjoint

added theorem connected_component_eq

added theorem connected_component_rel_iff

added def connected_component_setoid

added theorem continuous.image_connected_component_eq_singleton

added theorem continuous.image_connected_component_subset

added theorem continuous.image_eq_of_equiv

added def continuous.pi0_lift

added theorem continuous.pi0_lift_continuous

added theorem continuous.pi0_lift_factors

added theorem continuous.pi0_lift_unique

added def continuous.pi0_map

added theorem is_connected.subset_connected_component

added theorem is_preconnected.subset_connected_component

added theorem is_preconnected_connected_component

added def pi0

added theorem pi0_lift_unique'

added theorem pi0_preimage_image

added theorem pi0_preimage_singleton

added theorem preimage_connected_component_connected

deleted theorem subset_connected_component

added theorem totally_disconnected_space_iff_connected_component_singleton

added theorem totally_disconnected_space_iff_connected_component_subsingleton

Modified src/topology/path_connected.lean

Modified src/topology/separation.lean