English
A comprehensive theorem giving a general Realize equivalence for liftAt with arbitrary indices and substitutions.
Русский
Полное теоремное утверждение об общей эквивалентности реализации liftAt с произвольными индексами и подстановками.
LaTeX
$$$ \text{Realize}_{\text{liftAt}}(\phi; n, n', m) \iff \text{Realize}_{\text{shift}}(\phi; xs) $$$
Lean4
@[simp]
theorem realize_onBoundedFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] {n : ℕ} (ψ : L.BoundedFormula α n)
{v : α → M} {xs : Fin n → M} : (φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs := by
induction ψ with
| falsum => rfl
| equal => simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]; rfl
| rel =>
simp only [onBoundedFormula, realize_rel, LHom.map_onRelation, Function.comp_apply, realize_onTerm]
rfl
| imp _ _ ih1 ih2 => simp only [onBoundedFormula, ih1, ih2, realize_imp]
| all _ ih3 => simp only [onBoundedFormula, ih3, realize_all]
