Mathlib Changelog
v4
Changelog
About
Github
Theorem
regularSpace_generateFrom
Modification history
2025-11-14 20:42
Mathlib/Topology/Separation/Regular.lean
feat(Topology/Separation): condition for regularity given a subbasis (#31387)
Added
regularSpace_generateFrom
View on Github →