isMaximal

Mathlib.ModelTheory.Satisfiability

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.completeTheory.isMaximal

English

The complete theory of any nonempty structure is maximal (duplicate).

Русский

Полная теория любой ненулевой структуры максимальна (повтор).

LaTeX

$$$\\text{CompleteTheory}(M) \\text{ is maximal}$ (duplicate)$$

Lean4

theorem isMaximal [Nonempty M] : (L.completeTheory M).IsMaximal :=
  ⟨isSatisfiable L M, mem_or_not_mem L M⟩

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

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

Разделы

Аффилиация

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