DiophFn — Mathlib

English

A function is Diophantine if its graph is Diophantine.

Русский

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

LaTeX

$$$$ \\text{DiophFn}(f) \\equiv \\text{Dioph} \\{v : \\text{Option}(\\alpha) \\to \\mathbb{N} \\mid f( v \\circ \\text{some} ) = v( \\text{none} )\\} $$$$

Lean4

/-- A function is Diophantine if its graph is Diophantine. -/
def DiophFn (f : (α → ℕ) → ℕ) : Prop :=
  Dioph {v : Option α → ℕ | f (v ∘ some) = v none}

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