model_iff_subset_completeTheory

Mathlib.ModelTheory.Semantics

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

English

If M realizes T, then T is contained in the complete theory of M.

Русский

Если M реализует T, то T ⊆ полная теория M.

LaTeX

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

Lean4

theorem model_iff_subset_completeTheory : M ⊨ T ↔ T ⊆ L.completeTheory M :=
  T.model_iff

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

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

Разделы

Аффилиация

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