realize_equivSentence_symm_con — Mathlib

English

For φ: L.Formula α and relabel map g: α → β, the realization of (φ.relabel g) with v equals φ realized at v ∘ g.

Русский

Для φ: L.Formula α и отображения relabel g: α → β, реализация (φ.relabel g) под v равна реализации φ на v ∘ g.

LaTeX

$$$ (\phi^{\mathrm{relabel}\, g})^M(v) \iff \phi^M(v \circ g) $$$

Lean4

@[simp]
theorem realize_equivSentence_symm_con [L[[α]].Structure M] [(L.lhomWithConstants α).IsExpansionOn M]
    (φ : L[[α]].Sentence) : ((equivSentence.symm φ).Realize fun a => (L.con a : M)) ↔ φ.Realize M :=
  by
  simp only [equivSentence, _root_.Equiv.symm_symm, Equiv.coe_trans, Realize, BoundedFormula.realize_relabelEquiv,
    Function.comp]
  refine _root_.trans ?_ BoundedFormula.realize_constantsVarsEquiv
  rw [iff_iff_eq]
  congr 1 with (_ | a)
  · simp
  · cases a

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