fintype

Mathlib.Computability.TuringMachine

URI: https://scilib.ai/kg/mathlib#Turing.TM2to1.Γ'.fintype

English

If K is finite and each Γ(k) is finite, then Γ'(K,Γ) is finite.

Русский

Если K конечен и каждое Γ(k) конечно, то Γ'(K,Γ) конечно.

LaTeX

$$$\text{Fintype}(\Gamma')$$$

Lean4

instance fintype [DecidableEq K] [Fintype K] [∀ k, Fintype (Γ k)] : Fintype (Γ' K Γ) :=
  instFintypeProd _ _

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

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

Разделы

Аффилиация

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