sumArrowEquivProdArrow_apply_snd

Mathlib.Logic.Equiv.Prod

URI: https://scilib.ai/kg/mathlib#Equiv.sumArrowEquivProdArrow_apply_snd

English

For f : α ⊕ β → γ and b : β, (sumArrowEquivProdArrow α β γ f).2 b = f (inr b).

Русский

Для f : α ⊕ β → γ и b : β, (sumArrowEquivProdArrow α β γ f).snd b = f (inr b).

LaTeX

$$$(sumArrowEquivProdArrow \alpha \beta \gamma f).2 b = f (\text{inr } b)$$$

Lean4

@[simp]
theorem sumArrowEquivProdArrow_apply_snd {α β γ} (f : α ⊕ β → γ) (b : β) :
    (sumArrowEquivProdArrow α β γ f).2 b = f (inr b) :=
  rfl

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

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

Разделы

Аффилиация

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