Countable product of measurable spaces

[t6s]

We want to have a measurable space structure on countable products of measurable spaces.
It would be useful in formalizations of probability theory and statistics.

Some pointers:

• https://arxiv.org/pdf/2212.07246.pdf , page 4, footnote 9
• Srivastava, S.M. (1998). A Course on Borel Sets. Springer-Verlag, New York.

[affeldt-aist]

NB: we have a finite product of probability spaces in PR #1645