instSequentialSpace — Mathlib

English

The sum (disjoint union) of two sequential spaces is a sequential space.

Русский

Сумма двух последовательных пространств (дисъjoint объединение) остаётся последовательной.

LaTeX

$$$\text{SequentialSpace}(X) \land \text{SequentialSpace}(Y) \Rightarrow \text{SequentialSpace}(X \oplus Y)$$$

Lean4

/-- The sum (disjoint union) of two sequential spaces is a sequential space. -/
instance instSequentialSpace [SequentialSpace X] [SequentialSpace Y] : SequentialSpace (X ⊕ Y) :=
  .sup (.coinduced Sum.inl) (.coinduced Sum.inr)

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