prodSumDistrib_apply_left

Mathlib.Logic.Equiv.Sum

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

English

The distributive map sends (a, inl b) to inl (a,b).

Русский

Дистрибутивная карта отправляет (a, inl b) в inl (a,b).

LaTeX

$$$$\mathrm{prodSumDistrib}(\alpha,\beta,\gamma)(a,\mathrm{Sum.inl}(b)) = \mathrm{Sum.inl}(a,b). $$$$

Lean4

@[simp]
theorem prodSumDistrib_apply_left {α β γ} (a : α) (b : β) : prodSumDistrib α β γ (a, Sum.inl b) = Sum.inl (a, b) :=
  rfl

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

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

Разделы

Аффилиация

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