ofUnique — Mathlib

English

If α and β have unique elements, then α ≃ β.

Русский

Если у α и β имеется единственный элемент, то существует эквивалентность α ≃ β.

LaTeX

$$$[Unique(\alpha)] \land [Unique(\beta)] \Rightarrow \alpha \simeq \beta$$$

Lean4

/-- If both `α` and `β` have a unique element, then `α ≃ β`. -/
@[simps (attr := grind =)]
def ofUnique (α β : Sort _) [Unique.{u} α] [Unique.{v} β] : α ≃ β
    where
  toFun := default
  invFun := default
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

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