setOf_realize_onFormula — Mathlib

English

For φ in the language with constants, the realization of the symmetry of the sentence under equivSentence equals the realization of the sentence in the target language with the constants interpreted by v.

Русский

Для φ в языке с константами реализация симметрии предложения под equivSentence совпадает с реализацией самого предложения в целевом языке с константами, интерпретированными через v.

LaTeX

$$$ (equivSentence.symm \varphi)^M(v) \iff \Sentence.Realize M \varphi $$$

Lean4

@[simp]
theorem setOf_realize_onFormula [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α) :
    (setOf (φ.onFormula ψ).Realize : Set (α → M)) = setOf ψ.Realize :=
  by
  ext
  simp

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