sumAssoc_toEquiv

Mathlib.Topology.Constructions.SumProd

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

English

The toEquiv component of the sum associativity matches the standard Equiv.sumAssoc.

Русский

Компонент toEquiv равен стандартному Equiv.sumAssoc.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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