instFinite

Mathlib.Data.Fintype.Powerset

URI: https://scilib.ai/kg/mathlib#Set.instFinite

English

If α is finite, then Set α is finite.

Русский

Если α конечно, то Set α конечно.

LaTeX

$$$\\operatorname{Finite}(\\mathrm{Set}(\\alpha)).$$$

Lean4

instance instFinite [Finite α] : Finite (Set α) :=
  by
  cases nonempty_fintype α
  infer_instance

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

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

Разделы

Аффилиация

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