emptySum — Mathlib

English

The sum of a space Y with X is homeomorphic to X when Y is empty, realized by the standard swap isomorphism on sums.

Русский

Сумма пространства Y и X гомеоморфна X, когда Y пусто; реализуется обычной перестановкой в сумме.

LaTeX

$$$ (Y \\oplus X) \\cong_T X \\quad\\text{for } Y = \\varnothing $$$

Lean4

/-- The sum of `X` with any empty topological space is homeomorphic to `X`. -/
def emptySum [IsEmpty Y] : Y ⊕ X ≃ₜ X :=
  (sumComm Y X).trans (sumEmpty X Y)

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