mathlib3

71a9381e - feat(topology/instances/discrete): the discrete topology is metrizable (#17145)