English
A function f on Vector3 ℕ n is Diophantine iff the set {v | f(v ∘ fs) = v fz} is Diophantine.
Русский
Функция f на Vector3 ℕ n диагофантова тогда и только тогда, когда множество {v | f(v ∘ fs) = v fz} диагофантово.
LaTeX
$$$$\mathrm{DiophFn}(f) \iff \mathrm{Dioph}\left(\{v: Vector3 \mathbb{N} n \to \mathbb{N} \mid f(v \circ \mathrm{fs}) = v(\mathrm{fz})\}\right)$$$$
Lean4
theorem diophFn_vec (f : Vector3 ℕ n → ℕ) : DiophFn f ↔ Dioph {v | f (v ∘ fs) = v fz} :=
⟨reindex_dioph _ (fz ::ₒ fs), reindex_dioph _ (none :: some)⟩