English
If the language with constants and a corresponding homomorphism is expanded, the constants-variables equivalence preserves realization.
Русский
Расширение языка констант сохраняет реализацию через эквивалентность констант- переменных.
LaTeX
$$$ (constantsVarsEquiv \; \phi).Realize (Sum.elim (fun a \mapsto L.con a) v) xs \iff \phi.Realize v xs $$$
Lean4
theorem realize_constantsVarsEquiv [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M] {n}
{φ : L[[α]].BoundedFormula β n} {v : β → M} {xs : Fin n → M} :
(constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) v) xs ↔ φ.Realize v xs :=
by
refine
realize_mapTermRel_id (fun n t xs => realize_constantsVarsEquivLeft) fun n R xs =>
?_
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [← (lhomWithConstants L α).map_onRelation (Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n) R) xs]
rcongr
obtain - | R := R
· simp
· exact isEmptyElim R
