piUnique — Mathlib

English

If α has a unique element, then the function space α → β is equivalent to β.

Русский

Если у α есть уникальный элемент, то пространство функций α → β эквивалентно β.

LaTeX

$$$ (\alpha \to \beta) \simeq \beta \quad [\text{Unique } \alpha] $$$

Lean4

/-- The equivalence `(∀ i, β i) ≃ β ⋆` when the domain of `β` only contains `⋆` -/
@[simps (attr := grind =) -fullyApplied]
def piUnique [Unique α] (β : α → Sort*) : (∀ i, β i) ≃ β default
    where
  toFun f := f default
  invFun := uniqueElim
  left_inv f := by ext i; cases Unique.eq_default i; rfl

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