English
If φ is atomic and f is an injective homomorphism between structures, then φ.Realize commutes with f: φ.Realize v xs implies φ.Realize (f∘v) (f∘xs).
Русский
Если φ атомарна и f — инъективное гомоморфизм между структурами, то реализация φ сохраняется под применением f: φ.Realize v xs ⇒ φ.Realize (f∘v) (f∘xs).
LaTeX
$$$\varphi.IsAtomic \to (\text{Injective}(f) \Rightarrow (\varphi.Realize v xs \Rightarrow \varphi.Realize (f \circ v) (f \circ xs)))$$$
Lean4
theorem realize_comp_of_injective {φ : L.BoundedFormula α n} (hA : φ.IsAtomic) [L.HomClass F M N] {f : F}
(hInj : Function.Injective f) {v : α → M} {xs : Fin n → M} : φ.Realize v xs → φ.Realize (f ∘ v) (f ∘ xs) := by
induction hA with
| equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, hInj.eq_iff, imp_self]
| rel R ts =>
simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
