toSigma_mk

Mathlib.Data.Sigma.Basic

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

English

The image under toSigma of a pair (x,y) is the sigma pair ⟨x,y⟩.

Русский

Образ отображения toSigma от пары (x,y) есть ⟨x,y⟩.

LaTeX

$$$(x,y).toSigma = \\langle x, y \\rangle$$$

Lean4

@[simp]
theorem toSigma_mk {α β} (x : α) (y : β) : (x, y).toSigma = ⟨x, y⟩ :=
  rfl

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

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

Разделы

Аффилиация

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