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.