mathlib

7e20058e - feat(topology/Profinite/cofiltered_limit): Locally constant functions from cofiltered limits (#7992)

feat(topology/Profinite/cofiltered_limit): Locally constant functions from cofiltered limits (#7992) This generalizes one of the main technical theorems from LTE about cofiltered limits of profinite sets. This theorem should be useful for a future proof of Stone duality. Co-authored-by: Kyle Miller <kmill31415@gmail.com>