[Merged by Bors] - feat(Mathlib/Topology/Bases): subbasis closed under intersection is a basis#12221
Closed
mans0954 wants to merge 18 commits intomasterfrom mans0954/subbasis-closed-under-inter
Commits
Commits on Apr 17, 2024
Commits on Apr 18, 2024
- committed
Commits on Apr 26, 2024
Commits on May 2, 2024
Commits on May 11, 2024
Commits on May 19, 2024
Commits on May 25, 2024
Commits on Jun 1, 2024
Commits on Jun 7, 2024
Commits on Jun 15, 2024
Commits on Jun 23, 2024
Commits on Jun 29, 2024
Commits on Jul 12, 2024
Commits on Jul 13, 2024
Commits on Jul 14, 2024
- committed
- committed