addBottom_head_fst

Mathlib.Computability.TuringMachine

URI: https://scilib.ai/kg/mathlib#Turing.TM2to1.addBottom_head_fst

English

The first projection of the head of addBottom L is true.

Русский

Первая проекция головы addBottom L равна true.

LaTeX

$$$ (\mathrm{addBottom} \; L).\mathrm{head}.\mathrm{fst} = \text{true} $$$

Lean4

theorem addBottom_head_fst (L : ListBlank (∀ k, Option (Γ k))) : (addBottom L).head.1 = true := by
  rw [addBottom, ListBlank.head_cons]

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

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

Разделы

Аффилиация

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