instEmptyCollection

Mathlib.Data.Finset.Empty

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

English

There is an EmptyCollection instance for Finset α.

Русский

Существует инстанс пустой коллекции для Finset α.

LaTeX

$$\\text{EmptyCollection}(\\mathrm{Finset}(\\alpha))$$

Lean4

instance : EmptyCollection (Finset α) :=
  ⟨Finset.empty⟩

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

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

Разделы

Аффилиация

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