theory_model

Mathlib.ModelTheory.Semantics

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.ElementarilyEquivalent.theory_model

English

Two elementarily equivalent structures have the same nonempty status.

Русский

Пусть M и N элементарно эквивалентны; тогда непустость M эквивалентна непустости N.

LaTeX

$$L.ElementarilyEquivalent M N → (Nonempty M ↔ Nonempty N)$$

Lean4

theorem theory_model [MT : M ⊨ T] (h : M ≅[L] N) : N ⊨ T :=
  h.theory_model_iff.1 MT

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru