of_eq — Mathlib

English

Let f,g be partial functions from α to σ. If f is partial recursive and f and g agree at every input, then g is also partial recursive.

Русский

Пусть f,g — частичные функции от α к σ. Якщо f частично рекурсивна и f(n) = g(n) для всех n, то и g частично вычислима.

LaTeX

$$$\forall \alpha\sigma\,[\text{Primcodable }\alpha]\,[\text{Primcodable }\sigma]\;\forall f,g:\alpha\to^.\sigma:\ Partrec(f)\ \land\ (\forall n:\alpha,\ f(n)=g(n))\ \Rightarrow\ Partrec(g).$$

Lean4

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

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