refl

Mathlib.Computability.TuringDegree

URI: https://scilib.ai/kg/mathlib#TuringReducible.refl

English

A function is Turing reducible to itself; every f satisfies f ≤ᵀ f.

Русский

Любая функция сводима к самой себе; для каждого f выполняется f ≤ᵀ f.

LaTeX

$$$ \forall f: \mathbb{N} \to^. \mathbb{N}, \ f \le_T f $$$

Lean4

protected theorem refl (f : ℕ →. ℕ) : f ≤ᵀ f :=
  .oracle _ <| by simp

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

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

Разделы

Аффилиация

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