coe_sumMap

Mathlib.Logic.Embedding.Basic

URI: https://scilib.ai/kg/mathlib#Function.Embedding.coe_sumMap

English

The underlying function of sumMap is Sum.map: sumMap e1 e2 = Sum.map e1 e2 as functions.

Русский

Функция-основа у sumMap равна Sum.map: sumMap e1 e2 = Sum.map e1 e2.

LaTeX

$$$\\mathrm{Sum.map}(e_1,e_2) = \\mathrm{sumMap}(e_1,e_2)$$$

Lean4

@[simp]
theorem coe_sumMap {α β γ δ} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : sumMap e₁ e₂ = Sum.map e₁ e₂ :=
  rfl

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

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

Разделы

Аффилиация

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