Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-07 07:06 4a4cd6d6

View on Github →

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

Estimated changes