completeTheory_eq

Mathlib.ModelTheory.Semantics

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

English

Elementarily equivalent structures have the same complete theory.

Русский

Если M элементарно эквивалентна N, то их полные теории совпадают.

LaTeX

$$M ≡_L N ⇒ L.completeTheory M = L.completeTheory N$$

Lean4

theorem completeTheory_eq (h : M ≅[L] N) : L.completeTheory M = L.completeTheory N :=
  h

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

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

Разделы

Аффилиация

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