instSubsingleton

Mathlib.Logic.Unique

URI: https://scilib.ai/kg/mathlib#Unique.instSubsingleton

English

If α has a Unique instance, then α is a Subsingleton.

Русский

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

LaTeX

$$$\operatorname{Subsingleton}(\alpha)$$$

Lean4

instance (priority := 100) instSubsingleton : Subsingleton α :=
  subsingleton_of_forall_eq _ eq_default

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

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

Разделы

Аффилиация

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