nonempty_unique

Mathlib.Logic.Unique

URI: https://scilib.ai/kg/mathlib#nonempty_unique

English

If α is a subsingleton and nonempty, then there exists a Unique α.

Русский

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

LaTeX

$$$\\\\operatorname{Nonempty}(\\\\mathrm{Unique}(\\\\alpha))$$$

Lean4

theorem nonempty_unique (α : Sort u) [Subsingleton α] [Nonempty α] : Nonempty (Unique α) :=
  by
  inhabit α
  exact ⟨Unique.mk' α⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru