uniqueProd — Mathlib

English

If X is a topological space and Y is a singleton-type (Unique X), then X × Y is homeomorphic to X.

Русский

Если X — топологическое пространство, а Y — единичный тип (уникальный), то X × Y гомеоморфно X.

LaTeX

$$$\forall X,Y\ [TopologicalSpace X][TopologicalSpace Y][Unique X],\ X\times Y \cong_{\mathrm{Top}} X \quad\text{via } (x,y) \mapsto x.$$$

Lean4

/-- `X × {*}` is homeomorphic to `X`. -/
@[simps! symm_apply_snd]
def uniqueProd (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] [Unique X] : X × Y ≃ₜ Y :=
  (prodComm _ _).trans (prodUnique Y X)

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