instFintypeOne

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

For any type α with a distinguished element 1, the singleton {1} is finite.

Русский

Для любого типа α с особым элементом 1 множество {1} конечно.

LaTeX

$$$\text{For all } \alpha \text{ with } 1,\; \{1\} \text{ is finite}$$$

Lean4

@[to_additive]
instance instFintypeOne [One α] : Fintype (1 : Set α) :=
  Set.fintypeSingleton _

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

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

Разделы

Аффилиация

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