instTopologicalSpaceSum — Mathlib

English

The topology on the disjoint sum X ⊕ Y is the coarsest topology making the injections from X and Y continuous (coproduct topology).

Русский

Топология на дизъюнктном сумме X ⊕ Y является наименьшей по силе топологией, которая делает вложения из X и Y непрерывными (топология coproduct).

LaTeX

$$$\\text{Top}(X\\oplus Y) \\text{ is the coproduct topology: the injections } \\iota_X: X \\to X\\oplus Y \\text{ and } \\iota_Y: Y \\to X\\oplus Y \\text{ are continuous and generate the topology.}$$$

Lean4

instance instTopologicalSpaceSum [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y] : TopologicalSpace (X ⊕ Y) :=
  coinduced Sum.inl t₁ ⊔ coinduced Sum.inr t₂

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