apply₁ — Mathlib

English

Applying a unary function symbol f to a term t yields the term f(t). More precisely, the operation takes a unary function symbol and a term in α and returns the term in α formed by composing f with t.

Русский

Применение унарного символа функции f к терму t даёт терм f(t). Точнее, операция принимает унарный символь функции и терм в переменных α и возвращает терм в α, полученный из композиции f и t.

LaTeX

$$$\\forall f\\in L.Constructions(1),\\ \\forall t\\in L\\Term(\\alpha):\\ \\mathrm{apply}_1(f,t) = \\mathrm{func}\\ f\\!\\,[t]$$$

Lean4

/-- Applies a unary function to a term. -/
def apply₁ (f : L.Functions 1) (t : L.Term α) : L.Term α :=
  func f ![t]

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