Coproducts of Quasi-Borel Spaces

This file defines small coproducts of quasi-borel spaces by giving a QuasiBorelSpace instance for the Σ type.

See [HKSY17], Proposition 17.

@[instance_reducible]

instance QuasiBorelSpace.Sigma.instSigma {I : Type u_1} {P : I → Type u_2} [(i : I) → QuasiBorelSpace (P i)] : QuasiBorelSpace ((i : I) × P i)

Equations

• QuasiBorelSpace.Sigma.instSigma = { IsVar := fun (φ : ℝ → (i : I) × P i) => ∃ (ψ : QuasiBorelSpace.Sigma.Var I P), ∀ (r : ℝ), φ r = ↑ψ r, isVar_const := ⋯, isVar_comp := ⋯, isVar_cases' := ⋯ }

def Sigma.distrib {I : Type u_1} {P : I → Type u_2} {A : Type u_3} : A × Sigma P → (x : I) × A × P x

Equations

• Sigma.distrib (x_1, ⟨y, z⟩) = ⟨y, (x_1, z)⟩