English
A second formulation of composition for a vector of Diophantine functions is Dioph.
Русский
Вторая формулировка композиции для вектора диагофантовых функций диагофантова.
LaTeX
$$$$\mathrm{Dioph}(S) \Rightarrow \mathrm{Dioph}(\{v \mid \cdots\})$$$$
Lean4
theorem diophFn_comp {f : Vector3 ℕ n → ℕ} (df : DiophFn f) (g : Vector3 ((α → ℕ) → ℕ) n) (dg : VectorAllP DiophFn g) :
DiophFn fun v => f fun i => g i v :=
dioph_comp ((diophFn_vec _).1 df) ((fun v => v none) :: fun i v => g i (v ∘ some)) <|
by
simp only [vectorAllP_cons]
exact
⟨proj_dioph none, (vectorAllP_iff_forall _ _).2 fun i => reindex_diophFn _ <| (vectorAllP_iff_forall _ _).1 dg _⟩
