subsingleton_unique — Mathlib

English

Let α be any type. The type Unique α has exactly one element; in particular, any two elements of Unique α are equal.

Русский

Пусть α — произвольный тип. Тип Unique α состоит ровно из одного элемента; следовательно, любые два элемента Unique α равны.

LaTeX

$$$\\\\forall x,y : \\\\mathrm{Unique}(\\\\alpha),\\\\; x = y$$$

Lean4

instance subsingleton_unique : Subsingleton (Unique α) :=
  ⟨Unique.subsingleton_unique'⟩

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