instSubsingletonTrunc

Mathlib.Data.Quot

URI: https://scilib.ai/kg/mathlib#Trunc.instSubsingletonTrunc

English

The truncated type Trunc α has at most one element.

Русский

Усечённый тип Trunc α содержит не более одного элемента.

LaTeX

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

Lean4

instance instSubsingletonTrunc : Subsingleton (Trunc α) :=
  ⟨Trunc.eq⟩

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

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

Разделы

Аффилиация

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