coe_punitProd

Mathlib.Topology.UniformSpace.Equiv

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

English

The underlying function of the uniform equivalence punitProd is the second projection on PUnit × α.

Русский

Пусть подлежащая функция равномерного эквивалентности punitProd равна второй проекции на PUnit × α.

LaTeX

$$$\\operatorname{toFun}(punitProd\\,\\alpha) = \\operatorname{Prod.snd}$$$

Lean4

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

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

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

Разделы

Аффилиация

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