English
If f and g are Diophantine functions from (α → ℕ) → ℕ, then the function v ↦ f(v) − g(v) is Diophantine.
Русский
Если f и g — диофантовы функции, тогда функция v ↦ f(v) − g(v) также диофантова.
LaTeX
$$$$\\forall \\{\\alpha : Type\\} {f,g:(\\alpha \\to \\mathbb{N})\\to \\mathbb{N},\\;\\mathrm{DiophFn}\\,f \\to \\mathrm{DiophFn}\\,g \\to \\mathrm{DiophFn}\\bigl(\\lambda v. f(v)-g(v)\\bigr).$$$$
Lean4
/-- Diophantine functions are closed under subtraction. -/
theorem sub_dioph : DiophFn fun v => f v - g v :=
diophFn_comp2 df dg <|
(diophFn_vec _).2 <|
ext (D&1 D= D&0 D+ D&2 D∨ D&1 D≤ D&2 D∧ D&0 D= D.0) <|
(vectorAll_iff_forall _).1 fun x y z =>
show y = x + z ∨ y ≤ z ∧ x = 0 ↔ y - z = x from
⟨fun o => by
rcases o with (ae | ⟨yz, x0⟩)
· rw [ae, add_tsub_cancel_right]
· rw [x0, tsub_eq_zero_iff_le.mpr yz], by cutsat⟩
