Dioph — Mathlib

English

A partial function is Diophantine if its graph is Diophantine.

Русский

Частичная функция Диофова, если её граф диофова.

LaTeX

$$$$ \\text{DiophPFun}(f) \\;\\equiv\\; Dioph \\{v : \\text{Option}\\; \\alpha \\to \\mathbb{N} \\mid f\\bigl(v \\circ \\text{some}\\bigr) = v\\,\\text{none} \\} $$$$

Lean4

/-- A set `S ⊆ ℕ^α` is Diophantine if there exists a polynomial on
  `α ⊕ β` such that `v ∈ S` iff there exists `t : ℕ^β` with `p (v, t) = 0`. -/
def Dioph {α : Type u} (S : Set (α → ℕ)) : Prop :=
  ∃ (β : Type u) (p : Poly (α ⊕ β)), ∀ v, S v ↔ ∃ t, p (v ⊗ t) = 0

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