Commit 2025-11-03 12:38 9ab1fcc1
View on Github →feat(Topology): countable product of extended metric spaces (#30822) We already have a (highly non-canonical) (pseudo) metric space structure on a countable product of (pseudo) metric spaces. This PR factors that construction to first provide a (still highly non-canonical) (pseudo) extended metric space structure on a countable product of (pseudo) extended metric spaces.