CompletelyRegularSpace in Mathlib.Topology.CompletelyRegular
CompletelyRegularSpace
Mathlib.Topology.CompletelyRegular