realize_graph — Mathlib

English

Let f be an n-ary function symbol and x a sequence from Fin n to the domain; the graph of f realized at (y, x) matches the evaluation of the function Map at x giving y.

Русский

Пусть f — n-арный символь функции; граф графа f при аргументах y и x равен результату применения FunMap к x, получая y.

LaTeX

$$$ (\text{Formula.graph } f)^M(\text{Fin.cons } y\; x) \iff \text{funMap } f\; x = y $$$

Lean4

@[simp]
theorem realize_graph {f : L.Functions n} {x : Fin n → M} {y : M} :
    (Formula.graph f).Realize (Fin.cons y x : _ → M) ↔ funMap f x = y :=
  by
  simp only [Formula.graph, Term.realize, realize_equal, Fin.cons_zero, Fin.cons_succ]
  rw [eq_comm]

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