realize_function_term — Mathlib

English

For a function symbol f of arity n and a valuation v, the term f(t1,...,tn) realizes to the map sending i to realization of ti by v; i.e., f.term.realize v = funMap f v.

Русский

Для символа функции f арности n и значения v терм f(t1,...,tn) реализуется как отображение, отправляющее индекс i на реализацию ti при v; то есть f.term.realize v = funMap f v.

LaTeX

$$$\\operatorname{realize}_v(f^\\term) = \\operatorname{funMap} f\\; v$$$

Lean4

@[simp]
theorem realize_function_term {n} (v : Fin n → M) (f : L.Functions n) : f.term.realize v = funMap f v := by rfl

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