instFintype

Mathlib.Data.FinEnum

URI: https://scilib.ai/kg/mathlib#FinEnum.instFintype

English

A FinEnum α implies that α is finite (has a Fintype instance).

Русский

FinEnum α означает, что α конечен (существует структура Fintype).

LaTeX

$$$ [FinEnum\\ α] \\Rightarrow \\mathrm{Fintype}\\ α. $$$

Lean4

instance (priority := 100) [FinEnum α] : Fintype α
    where
  elems := univ.map (equiv).symm.toEmbedding
  complete := by intros; simp

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

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

Разделы

Аффилиация

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