univ_ofSubsingleton

Mathlib.Data.Fintype.OfMap

URI: https://scilib.ai/kg/mathlib#Fintype.univ_ofSubsingleton

English

If α is a subsingleton, then the universal finite set of α with base element a is {a}.

Русский

Если α — одноэлементный тип, то универсуальный набор равен {a}.

LaTeX

$$@univ _ (ofSubsingleton a) = { a }$$

Lean4

theorem univ_ofSubsingleton (a : α) [Subsingleton α] : @univ _ (ofSubsingleton a) = { a } :=
  rfl

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

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

Разделы

Аффилиация

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