coe_prodUnique — Mathlib

English

Let X and Y be topological spaces with Y a unique type. Then the product X × Y is homeomorphic to X, via the projection onto X.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coe_prodUnique [Unique Y] : ⇑(prodUnique X Y) = Prod.fst :=
  rfl

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