of_eq_tot

Mathlib.Computability.Partrec

URI: https://scilib.ai/kg/mathlib#Nat.Partrec.of_eq_tot

English

If f is Partrec and g(n) ∈ f(n) for all n, then g is Partrec.

Русский

Если f частично рекурсивна и g(n) ∈ f(n) для всех n, то g част partially rec.

LaTeX

$$$\text{Partrec } f \;\to\; (\forall n, g(n) \in f(n)) \to \text{Partrec } g.$$$

Lean4

theorem of_eq_tot {f : ℕ →. ℕ} {g : ℕ → ℕ} (hf : Partrec f) (H : ∀ n, g n ∈ f n) : Partrec g :=
  hf.of_eq fun n => eq_some_iff.2 (H n)

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

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

Разделы

Аффилиация

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