sumEmpty — Mathlib

English

The sum of a space X with an empty topological space Y is homeomorphic to X via the obvious equivalence that collapses the empty part.

Русский

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

LaTeX

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

Lean4

/-- The sum of `X` with any empty topological space is homeomorphic to `X`. -/
@[simps! -fullyApplied apply]
def sumEmpty [IsEmpty Y] : X ⊕ Y ≃ₜ X where
  toEquiv := Equiv.sumEmpty X Y
  continuous_toFun := Continuous.sumElim continuous_id (by fun_prop)
  continuous_invFun := continuous_inl

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