coe_uniqueProd

Mathlib.Logic.Equiv.Prod

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

English

The forward map of uniqueProd is the second projection: (b,a) ↦ a.

Русский

Промежуточное отображение uniqueProd равно проекции второго компонента: (b,a) ↦ a.

LaTeX

$$$$ (\\mathrm{uniqueProd}_{\\alpha,\\beta}) = \\mathrm{Prod.snd}. $$$$

Lean4

@[simp]
theorem coe_uniqueProd {α β} [Unique β] : (⇑(uniqueProd α β) : β × α → α) = Prod.snd :=
  rfl

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

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

Разделы

Аффилиация

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