coe_punitProd

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#Homeomorph.coe_punitProd

English

The underlying function of punitProd X is Prod.snd.

Русский

Базовая функция punitProd X равна Prod.snd.

LaTeX

$$$\mathrm{toFun}(\mathrm{punitProd} X) = \mathrm{Prod.snd}$$$

Lean4

@[simp]
theorem coe_punitProd : ⇑(punitProd X) = Prod.snd :=
  rfl

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

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

Разделы

Аффилиация

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