Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-18 11:09 5b579a2c

View on Github →

feat(topology/category/profinite): show Profinite is reflective in CompHaus (#6219) Show Profinite is reflective in CompHaus.

Estimated changes

Modified src/topology/category/CompHaus.lean

Modified src/topology/category/Profinite.lean

added def CompHaus.to_Profinite

added theorem CompHaus.to_Profinite_obj'

added def CompHaus.to_Profinite_obj

added def Profinite.to_CompHaus

added def Profinite.to_CompHaus_equivalence

added theorem Profinite.to_CompHaus_to_Top

added def Profinite.to_Profinite_adj_to_CompHaus

deleted def Profinite_to_CompHaus

deleted theorem Profinite_to_CompHaus_to_Top

Modified src/topology/connected.lean

added theorem connected_component_nrel_iff

added def connected_components

added theorem connected_components_lift_unique'

added theorem connected_components_preimage_image

added theorem connected_components_preimage_singleton

added def continuous.connected_components_lift

added theorem continuous.connected_components_lift_continuous

added theorem continuous.connected_components_lift_factors

added theorem continuous.connected_components_lift_unique

added def continuous.connected_components_map

added theorem continuous.connected_components_map_continuous

deleted def continuous.pi0_lift

deleted theorem continuous.pi0_lift_continuous

deleted theorem continuous.pi0_lift_factors

deleted theorem continuous.pi0_lift_unique

deleted def continuous.pi0_map

added theorem is_clopen.eq_union_connected_components

deleted def pi0

deleted theorem pi0_lift_unique'

deleted theorem pi0_preimage_image

deleted theorem pi0_preimage_singleton

Modified src/topology/separation.lean