funUnique — Mathlib

English

The same as Pi Unique specialized to functions, i.e., an equivalence between (α → β) and β when α is unique.

Русский

То же самое, что Pi Unique, но для функций: эквивалентность (α → β) и β, когда α уникально.

LaTeX

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

Lean4

/-- If `α` has a unique term, then the type of function `α → β` is equivalent to `β`. -/
@[simps! (attr := grind =) -fullyApplied apply symm_apply]
def funUnique (α β) [Unique.{u} α] : (α → β) ≃ β :=
  piUnique _

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