Commit 2022-01-11 13:55 8f5303ae

View on Github →

refactor(topology/connected): drop local attribute [instance] connected_component_setoid (#11365) Add a coercion from X to connected_components X instead.

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.disjoint_or_nonempty_inter

modified theorem set.not_disjoint_iff_nonempty_inter

Modified src/topology/category/Profinite/default.lean

Modified src/topology/connected.lean

deleted theorem connected_component_nrel_iff

deleted theorem connected_component_rel_iff

added theorem connected_components.coe_eq_coe'

added theorem connected_components.coe_eq_coe

added theorem connected_components.coe_ne_coe

added theorem connected_components.continuous_coe

added theorem connected_components.quotient_map_coe

added theorem connected_components.range_coe

added theorem connected_components.surjective_coe

modified theorem connected_components_lift_unique'

modified theorem connected_components_preimage_singleton

modified def continuous.connected_components_lift

added theorem continuous.connected_components_lift_apply_coe

added theorem continuous.connected_components_lift_comp_coe

modified theorem continuous.connected_components_lift_continuous

deleted theorem continuous.connected_components_lift_factors

modified theorem continuous.connected_components_lift_unique

added theorem continuous.image_eq_of_connected_component_eq

deleted theorem continuous.image_eq_of_equiv

added theorem disjoint_or_subset_of_clopen

added theorem is_clopen.bUnion_connected_component_eq

added theorem is_clopen.connected_component_subset

deleted theorem is_clopen.eq_union_connected_components

added theorem is_preconnected.subset_clopen

modified theorem is_preconnected_iff_subset_of_disjoint_closed

added theorem quotient_map.image_connected_component

added theorem quotient_map.preimage_connected_component

deleted theorem subset_or_disjoint_of_clopen

Modified src/topology/constructions.lean

added theorem continuous_quotient_lift_on'

Modified src/topology/separation.lean

modified theorem connected_component_eq_Inter_clopen

Modified src/topology/subset_properties.lean