prodPUnit

Mathlib.Topology.Constructions.SumProd

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

← MathLib Explorer

English

X × PUnit is naturally homeomorphic to X.

Русский

X × PUnit естественно гомеоморфно X.

LaTeX

$$$X \times PUnit \simeq_t X$$$

Lean4

/-- `X × {*}` is homeomorphic to `X`. -/
@[simps! -fullyApplied apply]
def prodPUnit : X × PUnit ≃ₜ X where
  toEquiv := Equiv.prodPUnit X
  continuous_toFun := continuous_fst
  continuous_invFun := .prodMk_left _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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