realize_onSentence — Mathlib

English

If φ is a L-homomorphism from L to L' and ψ is a sentence, then M satisfies φ.onSentence ψ iff M satisfies ψ.

Русский

Если φ — гомоморфизм языков L →ᴸ L' и ψ — предложение, то M ⊨ φ.onSentence ψ тогда и только тогда M ⊨ ψ.

LaTeX

$$$ M \models \phi.onSentence \psi \iff M \models \psi $$$

Lean4

@[simp]
theorem realize_onSentence [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Sentence) :
    M ⊨ φ.onSentence ψ ↔ M ⊨ ψ :=
  φ.realize_onFormula ψ

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