single

Mathlib.Computability.PostTuringMachine

URI: https://scilib.ai/kg/mathlib#Turing.Reaches₀.single

English

If b ∈ f a, then Reaches₀ f a b.

Русский

Если b принадлежит f a, то Reaches₀ f a b.

LaTeX

$$$\\mathrm{Option.instMembership.mem}(f\\ a,b)\\Rightarrow \\mathrm{Reaches_0}\\ f\\ a\\ b$$$

Lean4

theorem single {σ} {f : σ → Option σ} {a b : σ} (h : b ∈ f a) : Reaches₀ f a b
  | _, h₂ => h₂.head h

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

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

Разделы

Аффилиация

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