realize_subst — Mathlib

English

Substituting terms into a bounded formula preserves realizations: realizing φ.subst(tf) with v is equivalent to realizing φ with tf applied to v.

Русский

Замена переменных в ограниченной формуле сохраняет реализацию: реализация φ.subst(tf) равна реализации φ после подстановки tf в v.

LaTeX

$$$ (\phi.subst tf).Realize v xs \iff \phi.Realize (fun a \mapsto tf(a).realize v) xs $$$

Lean4

@[simp]
theorem realize_subst {φ : L.BoundedFormula α n} {tf : α → L.Term β} {v : β → M} {xs : Fin n → M} :
    (φ.subst tf).Realize v xs ↔ φ.Realize (fun a => (tf a).realize v) xs :=
  realize_mapTermRel_id
    (fun n t x => by
      rw [Term.realize_subst]
      rcongr a
      cases a
      · simp only [Sum.elim_inl, Function.comp_apply, Term.realize_relabel, Sum.elim_comp_inl]
      · rfl)
    (by simp)

Похожие утверждения