Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-09 06:11 c210d0fd

View on Github →

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.

Estimated changes