English
Let L be a language, M an L-structure, and consider a term t in the language whose variables are drawn from α ⊕ Fin n. For any m, n′ ∈ N and any valuation v on α ⊕ Fin(n+n′) into M, the realization of the lifted term t.liftAt n′ m under v equals the realization of t under a relabeled valuation: v composed with the canonical relabeling that inserts the newly added variables after the first m indices and shifts the remaining ones accordingly.
Русский
Пусть L — язык, M — структура над L, и возьмём терм t с переменными из α ⊕ Fin n. Для любых m, n′ ∈ ℕ и любой оценкu v на α ⊕ Fin(n+n′) в M, реализация поднятого терма t.liftAt n′ m по v равна реализации терма t по переопределённой оценке: v ∘ канонического переименования, вставляющего новые переменные после первых m индексов и смещающего остальные.
LaTeX
$$$ (t.liftAt n' m).realize\, v \;=\; t.realize\\left( v \\circ \\mathrm{Sum.map}\\left(\\mathrm{id}, \\lambda i : \\mathrm{Fin} _ { } \\Rightarrow \\text{if } \\uparrow i < m \\text{ then } \\mathrm{Fin.castAdd}\\ n' i \\text{ else } \\mathrm{Fin.addNat}\\ i n \\right) \\right) $$$
Lean4
@[simp]
theorem realize_liftAt {n n' m : ℕ} {t : L.Term (α ⊕ (Fin n))} {v : α ⊕ (Fin (n + n')) → M} :
(t.liftAt n' m).realize v =
t.realize (v ∘ Sum.map id fun i : Fin _ => if ↑i < m then Fin.castAdd n' i else Fin.addNat i n') :=
realize_relabel
