Commit 2026-05-04 19:24 415ab74a

View on Github →

feat(Topology): some lemmas about topological bases (#38538)

Estimated changes

Modified Mathlib/Topology/Bases.lean

added theorem TopologicalSpace.IsTopologicalBasis.continuousOn_iff

modified theorem TopologicalSpace.IsTopologicalBasis.isOpenMap_iff

added theorem TopologicalSpace.exists_seq_basis

added theorem TopologicalSpace.isTopologicalBasis_singleton_empty