mathlib3

dbb6b043 - feat(topology/separation): add lemma connected_component_eq_clopen_Inter (#5335)

feat(topology/separation): add lemma connected_component_eq_clopen_Inter (#5335) Prove the lemma that in a t2 and compact space, the connected component of a point equals the intersection of all its clopen neighbourhoods. Will be useful for work on Profinite sets. The proof that a Profinite set is a limit of finite discrete spaces found at: https://stacks.math.columbia.edu/tag/08ZY uses this lemma. Also some proofs that the category Profinite is reflective in CompactHausdorff uses this lemma. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>