coe_prodComm

Mathlib.Topology.UniformSpace.Equiv

URI: https://scilib.ai/kg/mathlib#UniformEquiv.coe_prodComm

English

The underlying function of prodComm is the swap map on pairs.

Русский

Обратная функция prodComm есть замена местами пары.

LaTeX

$$$\\forall {\\alpha} {\\beta} [UniformSpace \\alpha] [UniformSpace \\beta],\\; (prodComm \\alpha \\beta) = Prod.swap$$$

Lean4

@[simp]
theorem coe_prodComm : ⇑(prodComm α β) = Prod.swap :=
  rfl

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

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

Разделы

Аффилиация

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