subset

Mathlib.ModelTheory.Semantics

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

English

A structure M satisfies a theory T if and only if T is contained in the complete theory of M.

Русский

Структура M удовлетворяет теории T тогда и только тогда T ⊆ полная теория M.

LaTeX

$$$ M \models T \iff T \subseteq L^\mathrm{completeTheory}(M) $$$

Lean4

theorem subset [MT : M ⊨ T] : T ⊆ L.completeTheory M :=
  model_iff_subset_completeTheory.1 MT

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

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

Разделы

Аффилиация

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