diophPFun_vec — Mathlib

English

A vector-valued Diophantine partial function f on Vector3 ℕ n is equivalent to having a Diophantine representation of its graph.

Русский

Векторная диагофантова частичная функция эквивалентна диагофантовому графу.

LaTeX

$$$$\mathrm{DiophPFun}(f) \iff \mathrm{Dioph}\left(\{v \mid f.graph(v \circ \mathrm{fs}, v fz)\}\right)$$$$

Lean4

theorem diophPFun_vec (f : Vector3 ℕ n →. ℕ) : DiophPFun f ↔ Dioph {v | f.graph (v ∘ fs, v fz)} :=
  ⟨reindex_dioph _ (fz ::ₒ fs), reindex_dioph _ (none :: some)⟩

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