English
An elementary embedding preserves the realization of formulas under relabeling of variables.
Русский
Элементарное вложение сохраняет реализацию формул при перекодировке переменных.
LaTeX
$$$\varphi$ Realize (f ∘ x) ↔ $\varphi$ Realize x,$$
Lean4
@[simp]
theorem map_boundedFormula (f : M ↪ₑ[L] N) {α : Type*} {n : ℕ} (φ : L.BoundedFormula α n) (v : α → M) (xs : Fin n → M) :
φ.Realize (f ∘ v) (f ∘ xs) ↔ φ.Realize v xs := by
classical
rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id, iff_eq_eq]
have h :=
f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
(Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula, iff_eq_eq] at h
rw [← Function.comp_assoc _ _ (Fintype.equivFin _).symm,
Function.comp_assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _), _root_.Equiv.symm_comp_self, Function.comp_id,
Function.comp_assoc, Sum.elim_comp_inl, Function.comp_assoc _ _ Sum.inr, Sum.elim_comp_inr, ←
Function.comp_assoc] at h
refine h.trans ?_
erw [Function.comp_assoc _ _ (Fintype.equivFin _), _root_.Equiv.symm_comp_self, Function.comp_id, Sum.elim_comp_inl,
Sum.elim_comp_inr (v ∘ Subtype.val) xs, ←
Set.inclusion_eq_id (s := (BoundedFormula.freeVarFinset φ : Set α)) Set.Subset.rfl,
BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl]
