realize_equivSentence_symm — Mathlib

English

Symmetric version of realize_equivSentence_symm_con giving equivalence of realization for φ with α-constants and the symmetric equivSentence.

Русский

Симметричная версия realize_equivSentence_symm_con даёт эквивалентность реализации для φ с α-константами и симметричной equivSentence.

LaTeX

$$$ (equivSentence.symm φ)^M(v) \iff \text{Sentence.Realize } M φ $$$

Lean4

theorem realize_equivSentence_symm (φ : L[[α]].Sentence) (v : α → M) :
    (equivSentence.symm φ).Realize v ↔
      @Sentence.Realize _ M (@Language.withConstantsStructure L M _ α (constantsOn.structure v)) φ :=
  letI := constantsOn.structure v
  realize_equivSentence_symm_con M φ

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