instEmptyCollectionOfNatNat

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.instEmptyCollectionOfNatNat

English

Sym α 0 is a singleton type: it has exactly one element, the empty Sym.

Русский

Sym α 0 — это синглтон: ровно один элемент, пустое Sym.

LaTeX

$$$ |\mathrm{Sym}(\alpha,0)| = 1. $$$

Lean4

instance : EmptyCollection (Sym α 0) :=
  ⟨0⟩

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

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

Разделы

Аффилиация

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