English
If the term-relations maps ft and fr act as identities on realizations, then Realize of φ under v' xs equals Realize of φ under v xs.
Русский
Если отображения ft, fr сохраняют реализации, то реализация φ подменами не меняется.
LaTeX
$$$ (\phi.mapTermRel ft fr \dots).Realize v' xs \iff \phi.Realize v xs $$$
Lean4
theorem realize_mapTermRel_id [L'.Structure M] {ft : ∀ n, L.Term (α ⊕ (Fin n)) → L'.Term (β ⊕ (Fin n))}
{fr : ∀ n, L.Relations n → L'.Relations n} {n} {φ : L.BoundedFormula α n} {v : α → M} {v' : β → M} {xs : Fin n → M}
(h1 :
∀ (n) (t : L.Term (α ⊕ (Fin n))) (xs : Fin n → M), (ft n t).realize (Sum.elim v' xs) = t.realize (Sum.elim v xs))
(h2 : ∀ (n) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x) :
(φ.mapTermRel ft fr fun _ => id).Realize v' xs ↔ φ.Realize v xs := by
induction φ with
| falsum => rfl
| equal => simp [mapTermRel, Realize, h1]
| rel => simp [mapTermRel, Realize, h1, h2]
| imp _ _ ih1 ih2 => simp [mapTermRel, Realize, ih1, ih2]
| all _ ih => simp only [mapTermRel, Realize, ih, id]
