id_prod

Mathlib.Data.Prod.Basic

URI: https://scilib.ai/kg/mathlib#Prod.id_prod

English

The identity map on α × β equals the map sending p to (p1, p2).

Русский

Тождественное отображение на α × β равно отображению p ↦ (p1, p2).

LaTeX

$$$\\mathrm{id}_{\\\\alpha\\\\times\\\\beta} = (p \\\\mapsto (p.1, p.2)).$$$

Lean4

theorem id_prod : (fun p : α × β ↦ (p.1, p.2)) = id :=
  rfl

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

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

Разделы

Аффилиация

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