unique_iff_subsingleton_and_nonempty

English

There is a Unique α if and only if α is a subsingleton and nonempty.

Русский

Существует уникальный элемент типа α тогда и только тогда, когда α является субодиночным и непустым.

LaTeX

$$$\\\\operatorname{Nonempty}(\\\\mathrm{Unique}(\\\\alpha)) \\\\\\iff (\\\\operatorname{Subsingleton}(\\\\alpha) \\\\\\land \\\\operatorname{Nonempty}(\\\\alpha))$$$

Lean4

theorem unique_iff_subsingleton_and_nonempty (α : Sort u) : Nonempty (Unique α) ↔ Subsingleton α ∧ Nonempty α :=
  ⟨fun ⟨u⟩ ↦ by constructor <;> exact inferInstance, fun ⟨hs, hn⟩ ↦ nonempty_unique α⟩

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