Regularity of disjoint unions

Mathlib proves that a disjoint union Σ i, X i of Hausdorff spaces is Hausdorff (Sigma.t2Space). This file adds that a disjoint union of T₁ spaces is T₁ (Sigma.t1Space), which Mathlib does not provide, and that a disjoint union of regular spaces is regular (Sigma.regularSpace), so that a disjoint union of T₃ spaces is T₃. Each summand is an open and closed subspace, so a closed neighbourhood of a point inside its summand is a closed neighbourhood in the disjoint union.

Disjoint unions of disks are the spaces along which cells are attached to a cell complex, and their regularity is used to separate a point of an open cell from the rest of the complex.

instance Sigma.t1Space {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T1Space (X i)] : T1Space ((i : ι) × X i)

A disjoint union of T₁ spaces is T₁.

instance Sigma.regularSpace {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), RegularSpace (X i)] : RegularSpace ((i : ι) × X i)

A disjoint union of regular spaces is regular.