term — Mathlib

English

Every function symbol f of arity n can be represented as a term that uses n fresh variables indexed by Fin n. This is the standard way of encoding a symbol as a term.

Русский

Каждый символ функции arity n может быть представлен как терм, использующий n новых переменных, индексируемых по Fin n. Это стандартное кодирование символа как терма.

LaTeX

$$$\\forall n\\in \\mathbb{N},\\forall f\\in L.Functions(n):\\ \\mathrm{term}(f) = \\mathrm{func}\\ f\\ \\mathrm{var}^{(n)}$$$

Lean4

/-- The representation of a function symbol as a term, on fresh variables indexed by Fin. -/
def term {n : ℕ} (f : L.Functions n) : L.Term (Fin n) :=
  func f Term.var

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