continuousMapOfUnique — Mathlib

English

If X has a unique element, then Y is homeomorphic to C(X, Y).

Русский

Если у X существует единственный элемент, то Y гомеоморфно C(X, Y).

LaTeX

$$$Y \\cong_t C(X, Y)$$$

Lean4

/-- If `X` has a single element, then `Y` is homeomorphic to `C(X, Y)`. -/
def continuousMapOfUnique [Unique X] : Y ≃ₜ C(X, Y)
    where
  toFun := const X
  invFun f := f default
  right_inv
    f := by
    ext x
    rw [Unique.eq_default x]
    rfl
  continuous_toFun := continuous_const'
  continuous_invFun := continuous_eval_const _

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