homeomorphOfUnique — Mathlib

English

If both X and Y have a unique element, then there exists a homeomorphism between X and Y.

Русский

Если пространства X и Y имеют уникальные элементы, существует гомеоморфизм между ними.

LaTeX

$$$[Unique(X)] \land [Unique(Y)] \Rightarrow \exists h: X \simeq Y.$$$

Lean4

/-- If both `X` and `Y` have a unique element, then `X ≃ₜ Y`. -/
@[simps!]
def homeomorphOfUnique [Unique X] [Unique Y] : X ≃ₜ Y :=
  { Equiv.ofUnique X Y with
    continuous_toFun := continuous_const
    continuous_invFun := continuous_const }

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