instance BorelSpace.sum {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [TopologicalSpace α] [TopologicalSpace β] [BorelSpace α] [BorelSpace β] : BorelSpace (α ⊕ β)

instance BorelSpace.sigma {ι : Type u_3} {γ : ι → Type u_4} [(n : ι) → MeasurableSpace (γ n)] [(n : ι) → TopologicalSpace (γ n)] [∀ (n : ι), BorelSpace (γ n)] : BorelSpace ((n : ι) × γ n)

instance StandardBorelSpace.sum {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace α] [StandardBorelSpace β] : StandardBorelSpace (α ⊕ β)

A sum of two standard Borel spaces is standard Borel.

instance StandardBorelSpace.sigma_countable {ι : Type u_3} {γ : ι → Type u_4} [Countable ι] [(n : ι) → MeasurableSpace (γ n)] [∀ (n : ι), StandardBorelSpace (γ n)] : StandardBorelSpace ((n : ι) × γ n)

A sum of countably many standard Borel spaces is standard Borel.