English
For any QF formula φ, for any f, φ.Realize (f∘v) (f∘xs) is equivalent to φ.Realize v xs when f respects the structure (embedding class with strong homs).
Русский
Для любой QF-формулы φ и любого встраивания f: φ.Realize (f∘v) (f∘xs) эквивалентно φ.Realize v xs, если f сохраняет структуру (класс вложений и сильные гомоморфизмы).
LaTeX
$$$\text{IsQF}(\varphi) \to (\forall f\, (\varphi.Realize (f\circ v) (f\circ xs) \iff \varphi.Realize v xs))$$$
Lean4
theorem realize_embedding {φ : L.BoundedFormula α n} (hQF : φ.IsQF) (f : F) {v : α → M} {xs : Fin n → M} :
φ.Realize (f ∘ v) (f ∘ xs) ↔ φ.Realize v xs := by
induction hQF with
| falsum => rfl
| of_isAtomic hA =>
induction hA with
| equal t₁ t₂ =>
simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, (EmbeddingLike.injective f).eq_iff]
| rel R ts =>
simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
| imp _ _ ihφ ihψ => simp only [realize_imp, ihφ, ihψ]
