realize_onTerm — Mathlib

English

If φ : L.LHom L′ is an expansion map and t is a term in L, then applying φ to t and realizing yields the same as realizing t directly with v.

Русский

Если φ — отображение расширения между языками, и t — терм языка L, то реализация φ.onTerm(t) по v равна реализации t по v.

LaTeX

$$$ (\phi.onTerm t).realize\, v = t.realize\, v $$$

Lean4

@[simp]
theorem realize_onTerm [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (t : L.Term α) (v : α → M) :
    (φ.onTerm t).realize v = t.realize v := by
  induction t with
  | var => rfl
  | func f ts ih => simp only [Term.realize, LHom.onTerm, LHom.map_onFunction, ih]

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