Proposition. Borel sets and finite coordinate products [fdip-002E]
✍️source

  • October 25, 2026

For every finite real field space, \[\mathcal B(X_V)=\Sigma _V.\] Here \(\Sigma _V\) is the coordinate-product sigma-algebra. This finite-coordinate assertion, including dimension zero, follows by the direct argument below; compare [tao2011measure, Exercises 1.7.18-1.7.19, pp. 194-195, preliminary version].

Proof. 

  • October 25, 2026

Every evaluation is continuous by Definition [fdip-002C]. For fixed \(v\), the subsets of \(\mathbb R\) whose evaluation preimages are Borel form a sigma-algebra containing all open sets, hence all Borel sets. Thus each cylinder is Borel and \(\Sigma _V\subseteq \mathcal B(X_V)\).

Rational open intervals form a countable basis of \(\mathbb R\). Their finite coordinate products form a countable basis of \(X_V\). Each is a finite intersection of cylinder sets and belongs to \(\Sigma _V\). An arbitrary open set is the union of the basis elements it contains; this is a countable union, proving the reverse inclusion. For empty \(V\), the one basic box is the singleton itself, and both sigma-algebras are \(\{\varnothing ,X_V\}\).

Mathlib's Pi.borelSpace requires countable indices, second-countable topological factors and their Borel measurable structures. Finite real products meet these assumptions. The less restrictive pi_le_borel_pi gives only one inclusion, not the displayed equality.