Small Products of Quasi-Borel Spaces

This file defines small products of quasi-borel spaces by giving a QuasiBorelSpace instance for the · → · type.

See [HKSY17], Proposition 16.

instance QuasiBorelSpace.Pi.instForall {I : Type u_4} {P : I → Type u_5} [(i : I) → QuasiBorelSpace (P i)] : QuasiBorelSpace ((i : I) → P i)

Equations

• QuasiBorelSpace.Pi.instForall = { IsVar := fun (φ : ℝ → (i : I) → P i) => ∀ (i : I), QuasiBorelSpace.IsHom fun (x : ℝ) => φ x i, isVar_const := ⋯, isVar_comp := ⋯, isVar_cases' := ⋯ }

theorem QuasiBorelSpace.Pi.isHom_def {I : Type u_4} {P : I → Type u_5} [(i : I) → QuasiBorelSpace (P i)] (φ : ℝ → (i : I) → P i) : IsHom φ ↔ ∀ (i : I), IsHom fun (x : ℝ) => φ x i

theorem QuasiBorelSpace.Pi.isHom_apply {I : Type u_4} {P : I → Type u_5} [(i : I) → QuasiBorelSpace (P i)] (i : I) : IsHom fun (f : (i : I) → P i) => f i

theorem QuasiBorelSpace.Pi.isHom_pi {A : Type u_1} [QuasiBorelSpace A] {I : Type u_4} {P : I → Type u_5} [(i : I) → QuasiBorelSpace (P i)] {f : A → (i : I) → P i} (hf : ∀ (i : I), IsHom fun (x : A) => f x i) : IsHom f

@[simp]

theorem QuasiBorelSpace.Pi.isHom_iff {A : Type u_1} [QuasiBorelSpace A] {I : Type u_4} {P : I → Type u_5} [(i : I) → QuasiBorelSpace (P i)] {f : A → (i : I) → P i} : IsHom f ↔ ∀ (i : I), IsHom fun (x : A) => f x i

instance QuasiBorelSpace.Pi.instMeasurableQuasiBorelSpaceForall {I : Type u_4} {P : I → Type u_5} [(i : I) → QuasiBorelSpace (P i)] [(i : I) → MeasurableSpace (P i)] [∀ (i : I), MeasurableQuasiBorelSpace (P i)] : MeasurableQuasiBorelSpace ((i : I) → P i)