English
A vector-valued Diophantine partial function f on Vector3 ℕ n is equivalent to having a Diophantine representation of its graph.
Русский
Векторная диагофантова частичная функция эквивалентна диагофантовому графу.
LaTeX
$$$$\mathrm{DiophPFun}(f) \iff \mathrm{Dioph}\left(\{v \mid f.graph(v \circ \mathrm{fs}, v fz)\}\right)$$$$
Lean4
theorem diophPFun_vec (f : Vector3 ℕ n →. ℕ) : DiophPFun f ↔ Dioph {v | f.graph (v ∘ fs, v fz)} :=
⟨reindex_dioph _ (fz ::ₒ fs), reindex_dioph _ (none :: some)⟩