punitProd

Mathlib.Topology.Constructions.SumProd

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

English

Definition of a homeomorphism X × PUnit ≃ₜ X via prodComm and prodPUnit.

Русский

Определение гомеоморфизма X × PUnit ≃ₜ X через prodComm и prodPUnit.

LaTeX

$$$\text{prodPUnit}(X) : X \times PUnit \simeq_t X$$$

Lean4

/-- `{*} × X` is homeomorphic to `X`. -/
def punitProd : PUnit × X ≃ₜ X :=
  (prodComm _ _).trans (prodPUnit _)

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

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

Разделы

Аффилиация

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