mathlib

ee4fe743 - feat(topology/category/Profinite/cofiltered_clopen): Theorem about clopen sets in cofiltered limits of profinite sets (#7837)

feat(topology/category/Profinite/cofiltered_clopen): Theorem about clopen sets in cofiltered limits of profinite sets (#7837) This PR proves the theorem that any clopen set in a cofiltered limit of profinite sets arises from a clopen set in one of the factors of the limit. This generalizes a theorem used in LTE.