dioph_comp — Mathlib

English

Dioph is closed under composition: composing Dioph solvers yields a Dioph function.

Русский

Диоф сохраняется при композиции: композиция диагофантовых функций сохраняет диагофантовость.

LaTeX

$$$$\mathrm{Dioph}(S) \Rightarrow \mathrm{Dioph}(\{v \mid (f\,v) \circ (g\,v) \in S\})$$$$

Lean4

theorem dioph_comp {S : Set (Vector3 ℕ n)} (d : Dioph S) (f : Vector3 ((α → ℕ) → ℕ) n) (df : VectorAllP DiophFn f) :
    Dioph {v | (fun i => f i v) ∈ S} :=
  diophFn_compn (reindex_dioph _ inr d) df

Похожие утверждения