feat(topology/metric_space/metrizable): assume `regular_space` (#14586)
feat(topology/metric_space/metrizable): assume `regular_space` (#14586)






leanprover-community/mathlib,leanprover-community/mathlib