sumComm_symm

Mathlib.Topology.Constructions.SumProd

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

English

The swap map on sums is its own inverse.

Русский

Обмен компонент в сумме является собственным обратным.

LaTeX

$$$$ (\\mathrm{sumComm}\\,X\\,Y)^{-1} = \\mathrm{sumComm}\\,Y\\,X.$$$$

Lean4

@[simp]
theorem sumComm_symm : (sumComm X Y).symm = sumComm Y X :=
  rfl

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

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

Разделы

Аффилиация

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