Countable products of metrcs is metrizable

[zstone1]

Motivation for this change

Finally, we prove that countable products of metrics are metrizable! In particularly, the cantor set is metrizable. I have

• A definition for countable_uniformity. Several lemmas use it, so it made sense to factor into a nicer definition. Note that this property is equivalent to metrizability, so it has little purpose outside of this family of proofs.
• The main proof is that countable products preserve countable_uniformity. The definition of sup entourages is kinda annoying, so the proof is on the large side. It's not a blocker, just an inconvenience.
• A bunch of definitions to build mixins and types.

Things done/to do

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries, only append new ones, be careful: merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• [x] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.