Theorem TopologicalSpace.isTopologicalBasis_of_subbasis_of_finiteInter

Modification history

2024-07-15 16:11
Mathlib/Topology/Bases.lean
feat(Mathlib/Topology/Bases): subbasis closed under intersection is a basis (#12221) …
Added TopologicalSpace.isTopologicalBasis_of_subbasis_of_finiteInterView on Github →