elementarilyEquivalent_iff — Mathlib

English

Two L-structures M and N are elementarily equivalent if and only if they satisfy the same L-sentences; i.e., M ≅[L] N iff, for all φ, M ⊨ φ ⇔ N ⊨ φ.

Русский

Две структуры над языком L элементарно эквивалентны тогда и только тогда, когда выполняют одни и те же предложения L; то есть M ≅[L] N тогда и только тогда, когда для всех φ верно M ⊨ φ тогда и только N ⊨ φ.

LaTeX

$$$M \\cong_L N \\;\\iff\\; \\forall \\varphi \\in L\\text{-Sentence},\\; M \\models \\varphi \\leftrightarrow N \\models \\varphi$$$

Lean4

theorem elementarilyEquivalent_iff : M ≅[L] N ↔ ∀ φ : L.Sentence, M ⊨ φ ↔ N ⊨ φ := by
  simp only [ElementarilyEquivalent, Set.ext_iff, completeTheory, Set.mem_setOf_eq]

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