realize_functions_apply₂ — Mathlib

English

For a binary function symbol f and terms t1, t2, the realization of f(t1, t2) under v is the interpretation of f applied to the realizations of t1 and t2 under v.

Русский

Для бинарного символа функции f и термов t1, t2 реализация f(t1, t2) по v равна применению интерпретации f к реализациям t1 и t2 по v.

LaTeX

$$$ (f.apply₂ t₁ t₂).realize v = \mathrm{funMap}\, f\, ![t₁.realize\, v, t₂.realize\, v] $$$

Lean4

@[simp]
theorem realize_functions_apply₂ {f : L.Functions 2} {t₁ t₂ : L.Term α} {v : α → M} :
    (f.apply₂ t₁ t₂).realize v = funMap f ![t₁.realize v, t₂.realize v] :=
  by
  rw [Functions.apply₂, Term.realize]
  refine congr rfl (funext (Fin.cases ?_ ?_))
  · simp only [Matrix.cons_val_zero]
  · simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

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