English
For a term t and an index-substitution function f from t.varFinset to β, together with a valuation v′ on α, if v and v′ agree on the substituted variables, then the realization of t with restricted variables equals the realization of t with v′.
Русский
Для терма t и функции замены f, а также линейной оценки v′ на α, если v и v′ согласуются на заменённых переменных, тогда реализация t с ограниченными переменными равна реализации t с v′.
LaTeX
$$$ (t.restrictVar f).realize\, v = t.realize\, v' \quad\text{given } v' \text{ and } hv' : \forall a, v(f\,a) = v'(a) $$$
Lean4
theorem realize_restrictVar [DecidableEq α] {t : L.Term α} {f : t.varFinset → β} {v : β → M} (v' : α → M)
(hv' : ∀ a, v (f a) = v' a) : (t.restrictVar f).realize v = t.realize v' := by
induction t with
| var => simp [restrictVar, hv']
| func _ _ ih => exact congr rfl (funext fun i => ih i ((by simp [Function.comp_apply, hv'])))
