isComplete

Mathlib.ModelTheory.Satisfiability

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Theory.IsMaximal.isComplete

English

If T is maximal, then T is complete.

Русский

Если теория T максимальна, тогда она полна.

LaTeX

$$$T.isMaximal \\implies T.isComplete$$$

Lean4

theorem isComplete (h : T.IsMaximal) : T.IsComplete :=
  h.imp_right (forall_imp fun _ => Or.imp models_sentence_of_mem models_sentence_of_mem)

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

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

Разделы

Аффилиация

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