coe_prodMap

Mathlib.Logic.Embedding.Basic

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

English

The underlying function of prodMap is exactly Prod.map: the embedding e1.prodMap e2 equals Prod.map e1 e2.

Русский

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

LaTeX

$$$\\mathrm{prodMap}(e_1,e_2) = \\mathrm{Prod.map}(e_1,e_2)$$$

Lean4

@[simp]
theorem coe_prodMap {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : e₁.prodMap e₂ = Prod.map e₁ e₂ :=
  rfl

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

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

Разделы

Аффилиация

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