Coproducts of Quasi-Borel Spaces

This provides basic lemmas about the QuasiBorelSpace instance for the Σ type.

theorem QuasiBorelSpace.Sigma.isHom_def {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} (φ : ℝ → (i : I) × P i) : IsHom φ ↔ ∃ (ψ : Var I P), ∀ (r : ℝ), φ r = ↑ψ r

@[simp]

theorem QuasiBorelSpace.Sigma.isHom_mk {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} (i : I) : IsHom fun (x : P i) => ⟨i, x⟩

theorem QuasiBorelSpace.Sigma.isHom_elim {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} {A : Type u_5} {x✝¹ : QuasiBorelSpace A} {f : Sigma P → A} (hf : ∀ (i : I), IsHom fun (x : P i) => f ⟨i, x⟩) : IsHom f

theorem QuasiBorelSpace.Sigma.isHom_iff {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} {A : Type u_5} {x✝¹ : QuasiBorelSpace A} (f : Sigma P → A) : IsHom f ↔ ∀ (i : I), IsHom fun (x : P i) => f ⟨i, x⟩

@[simp]

theorem QuasiBorelSpace.Sigma.isHom_fst {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} [QuasiBorelSpace I] : IsHom Sigma.fst

@[simp]

theorem QuasiBorelSpace.Sigma.isHom_snd {I : Type u_1} {A : Type u_5} {x✝ : QuasiBorelSpace A} : IsHom Sigma.snd

@[simp]

theorem QuasiBorelSpace.Sigma.isHom_distrib {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} {A : Type u_5} {x✝¹ : QuasiBorelSpace A} : IsHom Sigma.distrib

theorem QuasiBorelSpace.Sigma.isHom_map {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} {J : Type u_3} {Q : J → Type u_4} {x✝¹ : (i : J) → QuasiBorelSpace (Q i)} {f : I → J} {g : (i : I) → P i → Q (f i)} (hg : ∀ (i : I), IsHom (g i)) : IsHom (Sigma.map f g)

instance QuasiBorelSpace.Sigma.instMeasurableQuasiBorelSpaceSigmaOfCountable {I : Type u_1} {P : I → Type u_2} {x✝ : (i : I) → QuasiBorelSpace (P i)} [Countable I] [(i : I) → MeasurableSpace (P i)] [∀ (i : I), MeasurableQuasiBorelSpace (P i)] : MeasurableQuasiBorelSpace (Sigma P)