univ_supports

Mathlib.Computability.PostTuringMachine

URI: https://scilib.ai/kg/mathlib#Turing.TM0.univ_supports

English

Any TM0 machine M is supported by the universal set Set.univ.

Русский

Любая машина TM0 поддерживается всеобщим множеством Set.univ.

LaTeX

$$$\\forall {\\Gamma} {\\Lambda},\\; \\mathrm{Supports}\\ M\\; \\mathrm{Set.univ}$$$

Lean4

theorem univ_supports (M : Machine Γ Λ) : Supports M Set.univ := by constructor <;> intros <;> apply Set.mem_univ

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

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

Разделы

Аффилиация

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