prodUnique — Mathlib

English

For any space X and a nonempty unique Y, the product X × Y is homeomorphic to X.

Русский

Для любой пара пространства X и единственного Y, множества X × Y гомеоморфно X.

LaTeX

$$$(X \\times Y) \\simeqₜ X$ for any unique Y$$

Lean4

/-- `X × {*}` is homeomorphic to `X`. -/
@[simps! symm_apply_snd]
def prodUnique [Unique Y] : X × Y ≃ₜ X where
  toEquiv := Equiv.prodUnique X Y
  continuous_toFun := continuous_fst
  continuous_invFun := continuous_id.prodMk continuous_const

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