DiophPFun — Mathlib

English

A partial function is Diophantine if its graph is Diophantine.

Русский

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

LaTeX

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

Lean4

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

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