English
If all fibers X i are Hausdorff, then the Sigma-type Σ i, X i is Hausdorff (with the appropriate topology).
Русский
Если все пространства X_i для индекса i — Хаусдорфовы, то сумма Σ_i X_i по σ-типу также Хаусдорфова.
LaTeX
$$$ \\left( \\forall i, TopologicalSpace(X_i) \\right) \\land \\left( \\forall i, T2Space(X_i) \\right) \\Rightarrow T2Space(\\Sigma i, X_i)$$$
Lean4
instance t2Space {ι} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ a, T2Space (X a)] : T2Space (Σ i, X i) :=
by
constructor
rintro ⟨i, x⟩ ⟨j, y⟩ neq
rcases eq_or_ne i j with (rfl | h)
· replace neq : x ≠ y := ne_of_apply_ne _ neq
exact separated_by_isOpenEmbedding .sigmaMk neq
· let _ := (⊥ : TopologicalSpace ι); have : DiscreteTopology ι := ⟨rfl⟩
exact separated_by_continuous (continuous_def.2 fun u _ => isOpen_sigma_fst_preimage u) h
