English
For a strong homomorphism g, bounded formulas satisfy realization invariance under composition with g: φ.Realize (g ∘ v) (g ∘ xs) ↔ φ.Realize v xs.
Русский
Для сильного гомоморфизма g реализации ограниченных формул сохраняются при композиции с g: φ.Realize (g ∘ v) (g ∘ xs) ↔ φ.Realize v xs.
LaTeX
$$$\varphi.Realize (g \circ v) (g \circ xs) \iff \varphi.Realize v xs$$$
Lean4
@[simp]
theorem realize_boundedFormula (φ : L.BoundedFormula α n) {v : α → M} {xs : Fin n → M} :
φ.Realize (g ∘ v) (g ∘ xs) ↔ φ.Realize v xs := by
induction φ with
| falsum => rfl
| equal => simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term, EmbeddingLike.apply_eq_iff_eq g]
| rel =>
simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
exact StrongHomClass.map_rel g _ _
| imp _ _ ih1 ih2 => rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]
| all _ ih3 =>
rw [BoundedFormula.Realize, BoundedFormula.Realize]
constructor
· intro h a
have h' := h (g a)
rw [← Fin.comp_snoc, ih3] at h'
exact h'
· intro h a
have h' := h (EquivLike.inv g a)
rw [← ih3, Fin.comp_snoc, EquivLike.apply_inv_apply g] at h'
exact h'
