coe_sigmaUnique

Mathlib.Logic.Equiv.Prod

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

English

The forward map of sigmaUnique is the first projection: (a,b) ↦ a.

Русский

Переходное отображение sigmaUnique равно проекции на первый компонент: (a,b) ↦ a.

LaTeX

$$$$ \\mathrm{coe}_{\\sigma\\_} = \\Sigma\\mathrm{fst}. $$$$

Lean4

@[simp]
theorem coe_sigmaUnique {α} {β : α → Type*} [∀ a, Unique (β a)] :
    (⇑(sigmaUnique α β) : (a : α) × (β a) → α) = Sigma.fst :=
  rfl

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

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

Разделы

Аффилиация

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