of_eq

Mathlib.Computability.Partrec

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

English

If f is Partrec and f n = g n for all n, then g is Partrec.

Русский

Если f частично рекурсивна и ∀n, f(n)=g(n), то g частично рекурсивна.

LaTeX

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

Lean4

theorem of_eq {f g : ℕ →. ℕ} (hf : Partrec f) (H : ∀ n, f n = g n) : Partrec g :=
  (funext H : f = g) ▸ hf

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

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

Разделы

Аффилиация

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