Commit 2025-12-03 09:57 ec491046
View on Github →feat: product of Borel spaces indexed by a subsingleton (#32274) A countable product of second countable Borel spaces is a Borel space, this is Pi.borelSpace. Here we drop the second countability assumption when the index type is a subsingleton.