realize_func — Mathlib

English

For a structure M and a valuation v, the interpretation of a function term f(t1,...,tn) is given by applying the interpretation of f to the interpretations of the subterms, i.e., realization distributes over function symbols.

Русский

Для структуры M и значения v трактовка терма функции f(t1,...,tn) равна применению трактовки функции f к трактовкам подтермов t1,...,tn.

LaTeX

$$$\\operatorname{realize}_v(\\operatorname{func} f\\ ts) = \\operatorname{funMap} f (\\lambda i. (ts(i)).\\operatorname{realize} v)$$$

Lean4

@[simp]
theorem realize_func (v : α → M) {n} (f : L.Functions n) (ts) :
    realize v (func f ts : L.Term α) = funMap f fun i => (ts i).realize v :=
  rfl

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