graph — Mathlib

English

The graph of a function f in a language with function symbols is the first-order formula asserting equality of the input argument with the value of the function on that argument.

Русский

Граф функции f в языке, содержащем функции, задаётся формулой, утверждающей равенство входного аргумента и значения функции на этом аргументе.

LaTeX

$$$\\text{graph}(f) = \\text{var}(0) = \\text{func}(f)(\\lambda i.\\text{var}(i+1))$$$

Lean4

/-- The graph of a function as a first-order formula. -/
def graph (f : L.Functions n) : L.Formula (Fin (n + 1)) :=
  Term.equal (var 0) (func f fun i => var i.succ)

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