Definitions/Def_Mathlib_MeasureTheory_Constructions_BorelSpace_RestrictedProduct.lean

Fix an index type \iota, a family of types R_i each carrying a topology, a family of subsets A_i \subseteq R_i, and a filter \mathcal{F} on \iota. The restricted product \Pi^r_{i}\,[R_i, A_i]_{[\mathcal{F}]} is the subspace of \prod_i R_i consisting of those families whose i-th coordinate lies in A_i for \mathcal{F}-eventually many i, with its restricted product topology. Two instances are declared on this space. The first equips it with the measurable space structure \mathrm{borel} of its topology, i.e. the \sigma-algebra generated by the open sets. The second records that this measurable space structure is a BorelSpace structure: the asserted compatibility is that the ambient \sigma-algebra coincides with the Borel \sigma-algebra of the topology, which holds by construction here. Consequently, for a restricted product the MeasurableSpace and BorelSpace typeclass searches succeed uniformly, so measurability of maps into and out of restricted products can be discussed in terms of the Borel structure, and the general Mathlib lemmas about Borel spaces (continuous functions are measurable, Borel-measurable sets are generated by the open sets, and so on) apply. Nothing further is asserted: in particular no comparison is made between this Borel \sigma-algebra and the \sigma-algebra generated by the coordinate projections, nor are any countability or second-countability hypotheses imposed on the factors, conditions under which such a comparison would be available.