prodComm_symm

Mathlib.Topology.Constructions.SumProd

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

English

The inverse of the associativity homeomorphism satisfies (prodAssoc X Y Z).symm = prodAssoc X Z Y.

Русский

Обратное отображение ассоциативности удовлетворяет (prodAssoc X Y Z).symm = prodAssoc X Z Y.

LaTeX

$$$(\mathrm{prodAssoc}\, X\, Y\, Z)^{\mathrm{symm}} = \mathrm{prodAssoc}\, X\, Z\, Y$$$

Lean4

@[simp]
theorem prodComm_symm : (prodComm X Y).symm = prodComm Y X :=
  rfl

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

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

Разделы

Аффилиация

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