sumComm

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#Homeomorph.sumComm

← MathLib Explorer

English

Disjoint sum is commutative up to homeomorphism.

Русский

Дизъюнктивная сумма коммутирует до гомеоморфизма.

LaTeX

$$$$\\mathrm{Homeomorph}.sumComm : X ⊕ Y ≃ₜ Y ⊕ X.$$$$

Lean4

/-- `X ⊕ Y` is homeomorphic to `Y ⊕ X`. -/
def sumComm : X ⊕ Y ≃ₜ Y ⊕ X where
  toEquiv := Equiv.sumComm X Y
  continuous_toFun := continuous_sum_swap
  continuous_invFun := continuous_sum_swap

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru