sigmaUnique_apply

Mathlib.Logic.Equiv.Prod

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

English

The forward map of sigmaUnique sends (a,b) to a.

Русский

Переходное отображение sigmaUnique отправляет (a,b) в a.

LaTeX

$$$$ \\mathrm{sigmaUnique}_{\\alpha,\\beta}(a,b) = a. $$$$

Lean4

theorem sigmaUnique_apply {α} {β : α → Type*} [∀ a, Unique (β a)] (x : (a : α) × β a) : sigmaUnique α β x = x.1 :=
  rfl

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

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

Разделы

Аффилиация

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