coe_uniqueProd — Mathlib

English

Let X and Y be topological spaces with X unique. Then X × Y is homeomorphic to Y, via the second projection.

Русский

Пусть X и Y — топологические пространства, X уникален. Тогда X × Y гомеоморфно Y через вторую проекцию.

LaTeX

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

Lean4

@[simp]
theorem coe_uniqueProd [Unique X] : ⇑(uniqueProd X Y) = Prod.snd :=
  rfl

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