sumSwap

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#IsOpenEmbedding.sumSwap

English

The swap map on a sum, Sum.swap: X ⊕ Y → Y ⊕ X, is an open embedding.

Русский

Отображение перестановки на сумме Sum.swap: X ⊕ Y → Y ⊕ X является открытым вложением.

LaTeX

$$$\\text{IsOpenEmbedding}(\\mathrm{Sum.swap})$$$

Lean4

theorem sumSwap : IsOpenEmbedding (@Sum.swap X Y) :=
  (Homeomorph.sumComm X Y).isOpenEmbedding

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

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

Разделы

Аффилиация

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