Proposition. Coordinate tests for measurable maps [fdip-002G]

Let \(V\) be finite and \((Y,\mathcal T)\) a measurable space. A map \(f:Y\to X_V\) is measurable if and only if every map \(y\mapsto f(y)(v)\) to the Borel real line is measurable. Continuous maps between finite real field spaces are Borel measurable. In particular this holds for linear maps, coordinate restriction, zero extension and polynomial functions. Compare [tao2011measure, Exercise 1.4.29 and Remark 1.4.33, pp. 95-96, preliminary version].

The product-measurability equivalence is measurable_pi_iff; it concerns measurable products, without asserting topology or integrability. For Borel spaces an inducing map also detects measurability through composition, as in Topology.IsInducing.measurable_comp_iff; no measurable range is required. Neither statement attaches a state to every observable.