sumCongr_apply

Mathlib.Logic.Equiv.Sum

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

English

The action of sumCongr on x is given by Sum.map of the component bijections.

Русский

Действие sumCongr на x задаётся как отображение Sum.map на компонентах биекций.

LaTeX

$$sumCongr ea eb x = Sum.map (↑ea) (↑eb) x$$

Lean4

@[simp]
theorem sumCongr_apply {α β} (ea : Equiv.Perm α) (eb : Equiv.Perm β) (x : α ⊕ β) :
    sumCongr ea eb x = Sum.map (⇑ea) (⇑eb) x :=
  rfl

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

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

Разделы

Аффилиация

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