instSubsingleton

Mathlib.Order.BoundedOrder.Basic

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

English

The Subsingleton property holds for the BoundedOrder type as well.

Русский

Свойство Subsingleton сохраняется и для типа BoundedOrder.

LaTeX

$$$\forall \alpha, Subsingleton (BoundedOrder \alpha)$$$

Lean4

instance instSubsingleton : Subsingleton (BoundedOrder α) where
  allEq := by rintro ⟨⟩ ⟨⟩; congr <;> exact Subsingleton.elim _ _

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

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

Разделы

Аффилиация

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