English
The set of places where two Diophantine functions are congruent modulo a third is Diophantine.
Русский
Множество мест, где две диофантовы функции эквивалентны по модулю третьей, является диофантовым.
LaTeX
$$$$\\forall {f,g:(\\alpha\\to\\mathbb{N})\\to \\mathbb{N},\\;\\mathrm{DiophFn}\\,f \\to \\mathrm{DiophFn}\\,g \\to \\forall {h:(\\alpha\\to\\mathbb{N})\\to\\mathbb{N},\\;\\mathrm{DiophFn}\\,h \\to \\mathrm{Dioph}\\,\\bigl(\\lambda v. f(v) \\equiv g(v) \\\\[MOD\\] h(v)\\bigr).$$$$
Lean4
/-- The set of places where two Diophantine functions are congruent modulo a third
is Diophantine. -/
theorem modEq_dioph {h : (α → ℕ) → ℕ} (dh : DiophFn h) : Dioph fun v => f v ≡ g v [MOD h v] :=
df D% dh D= dg D% dh
