English
If f and g are DiophFn, then the predicate 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{Dioph}\\,\\bigl(\\lambda v. f(v) \\mid g(v)\\bigr).$$$$
Lean4
/-- The set of places where one Diophantine function divides another is Diophantine. -/
theorem dvd_dioph : Dioph fun v => f v ∣ g v :=
dioph_comp ((D∃) 2 <| D&2 D= D&1 D* D&0) [f, g] ⟨df, dg⟩