English
For a unary function symbol f and a term t, the realization of f(t) under v is obtained by applying the interpretation of f to the realization of t under v. Similarly, for a binary function symbol f and terms t1, t2, the realization of f(t1, t2) under v is obtained by applying the interpretation of f to the pair of realizations of t1 and t2.
Русский
Для унарного символа функции f и терма t реализация f(t) по v равна применению интерпретации f к реализации t по v; для бинарного символа f реализация f(t1, t2) равна применению интерпретации f к упорядоченной паре реализаций t1 и t2.
LaTeX
$$$ (f.apply_1 t).realize v = \mathrm{funMap}\, f\, ![t.realize\, v] $$$
Lean4
@[simp]
theorem realize_functions_apply₁ {f : L.Functions 1} {t : L.Term α} {v : α → M} :
(f.apply₁ t).realize v = funMap f ![t.realize v] :=
by
rw [Functions.apply₁, Term.realize]
refine congr rfl (funext fun i => ?_)
simp only [Matrix.cons_val_fin_one]
