prodAssoc_toEquiv

Mathlib.Topology.Constructions.SumProd

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

English

The toEquiv field of prodAssoc equals Equiv.prodAssoc.

Русский

Поле toEquiv гомеоморфизма prodAssoc совпадает с Equiv.prodAssoc.

LaTeX

$$$(\mathrm{prodAssoc} X Y Z).toEquiv = \mathrm{Equiv.prodAssoc} X Y Z$$$

Lean4

@[simp]
theorem prodAssoc_toEquiv : (prodAssoc X Y Z).toEquiv = Equiv.prodAssoc X Y Z :=
  rfl

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

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

Разделы

Аффилиация

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