instSequentialSpace — Mathlib

English

The disjoint union of an indexed family of sequential spaces is sequential.

Русский

Объединение по индексу семейств последовательных пространств остаётся последовательной.

LaTeX

$$$\text{SequentialSpace}(X_i)\;\forall i \Rightarrow \text{SequentialSpace}(\Sigma i, X_i)$$$

Lean4

/-- The disjoint union of an indexed family of sequential spaces is a sequential space. -/
instance instSequentialSpace {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SequentialSpace (X i)] :
    SequentialSpace (Σ i, X i) :=
  .iSup fun _ ↦ .coinduced _

Похожие утверждения