inhabitedFinset

Mathlib.Data.Finset.Empty

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

English

The Finsetα has an EmptyCollection instance defined via Finset.empty.

Русский

Для Finset α определён инстансEmptyCollection через пустой Finset.

LaTeX

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

Lean4

instance inhabitedFinset : Inhabited (Finset α) :=
  ⟨∅⟩

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

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

Разделы

Аффилиация

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