uniqueEquivEquivUnique — Mathlib

English

If β has a unique element, then Unique α is equivalent to α ≃ β.

Русский

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

LaTeX

$$$Unique\\alpha\\ \\simeq\\ (\\alpha\\simeq\\beta)\\quad[Unique\\beta].$$$

Lean4

/-- If `Unique β`, then `Unique α` is equivalent to `α ≃ β`. -/
def uniqueEquivEquivUnique (α : Sort u) (β : Sort v) [Unique β] : Unique α ≃ (α ≃ β) :=
  equivOfSubsingletonOfSubsingleton (fun _ => Equiv.ofUnique _ _) Equiv.unique

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