funUnique — Mathlib

English

Evaluation at the unique point gives the homeomorphism in the PiUnique case.

Русский

Понижение по уникальной точке задает гомеоморфизм в случае PiUnique.

LaTeX

$$$ (\iota \to X) \to X,\; f \mapsto f(\text{default}). $$$

Lean4

/-- If `ι` has a unique element, then `ι → X` is homeomorphic to `X`. -/
@[simps! -fullyApplied]
def funUnique (ι X : Type*) [Unique ι] [TopologicalSpace X] : (ι → X) ≃ₜ X
    where
  toEquiv := Equiv.funUnique ι X
  continuous_toFun := continuous_apply _
  continuous_invFun := continuous_pi fun _ => continuous_id

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