mathlib

18f53db5 - feat(topology/metric_space/pi_nat): metric structure on product spaces (#12220)

feat(topology/metric_space/pi_nat): metric structure on product spaces (#12220) We endow the spaces `Π (n : ℕ), E n` or `Π (i : ι), E i` with various distances (not registered as instances), and use these to show that these spaces retract on their closed subsets.