mathlib3

c210d0fd - feat(topology/category/limits): Topological bases in cofiltered limits (#7820)

feat(topology/category/limits): Topological bases in cofiltered limits (#7820) This PR proves a theorem which provides a simple characterization of certain topological bases in a cofiltered limit of topological spaces. Eventually I will specialize this assertion to the case where the topological spaces are profinite, and the `T i` are the topological bases given by clopen sets. This generalizes a lemma from LTE. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>