Mathlib Changelog
v4
Changelog
About
Github
Theorem
Topology.WithGeneratedByTopology.isClosed_iff
Modification history
2025-10-24 15:50
Mathlib/Topology/Convenient/GeneratedBy.lean
feat(Topology): the topology generated by a family of spaces (#29341) …
Added
Topology.WithGeneratedByTopology.isClosed_iff
View on Github →