univ

Mathlib.Data.Fintype.Defs

URI: https://scilib.ai/kg/mathlib#Finset.univ

English

The universal finite set of α is the finite set of all elements of α.

Русский

Универсальный конечный набор α — это множество всех элементов α.

LaTeX

$$$$ \uparrow(\mathrm{univ} : \mathrm{Finset} \; \alpha) = \mathrm{Set.univ} $$$$

Lean4

/-- `univ` is the universal finite set of type `Finset α` implied from
  the assumption `Fintype α`. -/
def univ : Finset α :=
  @Fintype.elems α _

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

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

Разделы

Аффилиация

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