realize_relabelEquiv — Mathlib

English

A variant of the constants-equivariant realization when using the with-constants extension is preserved.

Русский

Вариант эквивалентности константной реализации для расширения withConstants сохраняется.

LaTeX

$$$ (constantsVarsEquiv \; \phi).Realize (Sum.elim (fun a => L.con a) v) xs \iff \phi.Realize v xs $$$

Lean4

@[simp]
theorem realize_relabelEquiv {g : α ≃ β} {k} {φ : L.BoundedFormula α k} {v : β → M} {xs : Fin k → M} :
    (relabelEquiv g φ).Realize v xs ↔ φ.Realize (v ∘ g) xs :=
  by
  simp only [relabelEquiv, mapTermRelEquiv_apply, Equiv.coe_refl]
  refine realize_mapTermRel_id (fun n t xs => ?_) fun _ _ _ => rfl
  simp only [relabelEquiv_apply, Term.realize_relabel]
  refine congr (congr rfl ?_) rfl
  ext (i | i) <;> rfl

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