diophFn_vec — Mathlib

English

A function f on Vector3 ℕ n is Diophantine iff the set {v | f(v ∘ fs) = v fz} is Diophantine.

Русский

Функция f на Vector3 ℕ n диагофантова тогда и только тогда, когда множество {v | f(v ∘ fs) = v fz} диагофантово.

LaTeX

$$$$\mathrm{DiophFn}(f) \iff \mathrm{Dioph}\left(\{v: Vector3 \mathbb{N} n \to \mathbb{N} \mid f(v \circ \mathrm{fs}) = v(\mathrm{fz})\}\right)$$$$

Lean4

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

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