Commit 2022-01-06 09:57 c391512e

feat(topology/metric_space/kuratowski): make the Kuratowski embedding have codomain the "true" ℓ^∞(ℕ) (#11280) (Previously, we didn't have the "true" ℓ^∞(ℕ), so we used the space of bounded continuous functions on ℕ equipped with the discrete topology.)