realize_sentence — Mathlib

English

Sentences have the same truth value in elementarily equivalent structures.

Русский

Если M и N элементарно эквивалентны, то для любого предложения φ верно M ⊨ φ тогда и только тогда, когда N ⊨ φ.

LaTeX

$$∀φ (M ≡_L N → (M ⊨ φ ↔ N ⊨ φ))$$

Lean4

theorem realize_sentence (h : M ≅[L] N) (φ : L.Sentence) : M ⊨ φ ↔ N ⊨ φ :=
  (elementarilyEquivalent_iff.1 h) φ

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