fintype

Mathlib.Computability.Encoding

URI: https://scilib.ai/kg/mathlib#Computability.Γ.fintype

English

The state type Γ of a finite encoding is finite.

Русский

Тип состояний Γ кодирования конечного типа является конечным.

LaTeX

$$$ | \\Gamma| < \infty $$$

Lean4

instance fintype {α : Type u} (e : FinEncoding α) : Fintype e.toEncoding.Γ :=
  e.ΓFin

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

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

Разделы

Аффилиация

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