instSingleton

Mathlib.Data.Ordmap.Ordset

URI: https://scilib.ai/kg/mathlib#Ordset.instSingleton

English

There is a Singleton instance giving Ordset a canonical singleton constructor.

Русский

Существует экземпляр Singleton, задающий канонический конструктор одиночного Ordset.

LaTeX

$$$\\mathrm{Ordset}.instSingleton : \\mathrm{Singleton}(\\alpha, \\mathrm{Ordset}(\\alpha))$$$

Lean4

instance instSingleton : Singleton α (Ordset α) :=
  ⟨Ordset.singleton⟩

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

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

Разделы

Аффилиация

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