sumCongr_refl

Mathlib.Logic.Equiv.Sum

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.sumCongr_refl

English

The sumCongr of identity permutations is the identity on the sum type.

Русский

Суммарное соответствие переходной единицы — единица на α ⊕ β.

LaTeX

$$sumCongr_refl {α β} : sumCongr (refl α) (refl β) = refl (Sum α β)$$

Lean4

theorem sumCongr_refl {α β} : sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β) :=
  Equiv.sumCongr_refl

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

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

Разделы

Аффилиация

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