refl

Mathlib.Computability.PostTuringMachine

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

English

For any a, Reaches₀ f a a holds (reflexivity).

Русский

Для любого a выполняется Reaches₀ f a a (рефлексивность).

LaTeX

$$$\\forall a:\\; Reaches_0\\ f\\ a\\ a$$$

Lean4

@[refl]
theorem refl {σ} {f : σ → Option σ} (a : σ) : Reaches₀ f a a
  | _, h => h

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

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

Разделы

Аффилиация

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