realize_equivSentence — Mathlib

English

For φ in L.Formula α, the realization of equivSentence φ equals the Realize of φ with constants interpreted by L.con.

Русский

Для φ в L.Formula α реализация equivSentence φ равна реализации φ с константами, интерпретируемыми через L.con.

LaTeX

$$$ \text{Realize}_M(\text{equivSentence }(\varphi)) \iff \text{Realize}_M(\varphi) \text{ with constants } (L.con) $$$

Lean4

@[simp]
theorem realize_equivSentence [L[[α]].Structure M] [(L.lhomWithConstants α).IsExpansionOn M] (φ : L.Formula α) :
    (equivSentence φ).Realize M ↔ φ.Realize fun a => (L.con a : M) := by
  rw [← realize_equivSentence_symm_con M (equivSentence φ), _root_.Equiv.symm_apply_apply]

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