instance
instMeasurableSpaceRestrictedProduct_fLT
{ι : Type u_1}
(R : ι → Type u_2)
(A : (i : ι) → Set (R i))
(𝓕 : Filter ι)
[(i : ι) → TopologicalSpace (R i)]
:
MeasurableSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕)
Equations
instance
instBorelSpaceRestrictedProduct_fLT
{ι : Type u_1}
(R : ι → Type u_2)
(A : (i : ι) → Set (R i))
(𝓕 : Filter ι)
[(i : ι) → TopologicalSpace (R i)]
:
BorelSpace (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕)