theory_model_iff — Mathlib

English

Elementarily equivalent structures model the same theories.

Русский

Если M эквивалентна N по языку L, тогда M моделирует теорию T тогда и только тогда, когда N моделирует T.

LaTeX

$$M ≅_L N → (M ⊨ T ↔ N ⊨ T)$$

Lean4

theorem theory_model_iff (h : M ≅[L] N) : M ⊨ T ↔ N ⊨ T := by
  rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory, h.completeTheory_eq]

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