of_eq — Mathlib

English

If two functions f,g are Pointwise equal and f is primitive recursive, then g is primitive recursive as well.

Русский

Если две функции f,g равны по каждой точке и f является примитивно-рекурсивной, то и g является примитивно-рекурсивной.

LaTeX

$$$$\\text{hf} : \\text{Primrec}(f) \\quad \\Rightarrow\\quad \\forall n, f(n)=g(n) \\Rightarrow \\text{Primrec}(g).$$$$

Lean4

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

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