unique_iff_existsUnique — Mathlib

English

For any type α, Nonempty (Unique α) is equivalent to ExistsUnique a with True.

Русский

Для любого типа α существование единственного элемента эквивалентно существованию ровно одного элемента satisfying True.

LaTeX

$$$\operatorname{Nonempty}(\\operatorname{Unique}(\alpha)) \iff \exists! a: \alpha, True$$$

Lean4

theorem unique_iff_existsUnique (α : Sort u) : Nonempty (Unique α) ↔ ∃! _ : α, True :=
  ⟨fun ⟨u⟩ ↦ ⟨u.default, trivial, fun a _ ↦ u.uniq a⟩, fun ⟨a, _, h⟩ ↦ ⟨⟨⟨a⟩, fun _ ↦ h _ trivial⟩⟩⟩

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