English
For Vector3-nary inputs, the Diophantine closure holds: if S is Dioph, then {v | (f v :: v) ∈ S} is Dioph for f DiophFn.
Русский
Для векторного случая, если S диагофантово, то множество {v | (f v :: v) ∈ S} диагофантово для DiophFn f.
LaTeX
$$$$\mathrm{Dioph}(S) \Rightarrow \mathrm{Dioph}\left(\{v: Vector3 \mathbb{N} n \to \mathbb{N} \mid (f v :: v) \in S\}\right)$$$$
Lean4
theorem diophFn_vec_comp1 {S : Set (Vector3 ℕ (succ n))} (d : Dioph S) {f : Vector3 ℕ n → ℕ} (df : DiophFn f) :
Dioph {v : Vector3 ℕ n | (f v :: v) ∈ S} :=
Dioph.ext (diophFn_comp1 (reindex_dioph _ (none :: some) d) df)
(fun v =>
by
dsimp
-- TODO: `apply iff_of_eq` is required here, even though `congr!` works on iff below.
apply iff_of_eq
congr 1
ext x; cases x <;> rfl)
