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_generateFromView on Github →