prod_snd_fst

Mathlib.Algebra.Notation.Pi.Defs

URI: https://scilib.ai/kg/mathlib#Pi.prod_snd_fst

English

The product map with second then first projection equals the swap: Pi.prod Prod.snd Prod.fst = .swap.

Русский

Производя сначала вторую, затем первую проекции, получаем перестановку: Pi.prod Prod.snd Prod.fst = .swap.

LaTeX

$$$\Pi.prod (Prod.snd) (Prod.fst) = .swap$$$

Lean4

theorem prod_snd_fst : Pi.prod (Prod.snd : α × β → β) (Prod.fst : α × β → α) = .swap :=
  rfl

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

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

Разделы

Аффилиация

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