Commit 2024-07-15 16:11 23f4d4ac

feat(Mathlib/Topology/Bases): subbasis closed under intersection is a basis (#12221) We show that if a sub-basis is closed under finite intersections, then it is a basis for a topology. As a corollary, if a sub-basis is closed under intersections, then inserting the universal set gives a basis for the topology. An example application of this result is given in #12234