theory_model

Mathlib.ModelTheory.ElementarySubstructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.ElementarySubstructure.theory_model

English

If M satisfies T, then any L-elementary substructure S of M also satisfies T.

Русский

Если M удовлетворяет теории T, то любая элементарная подструктура S M удовлетворяет T.

LaTeX

$$$M ⊨ T \Rightarrow S ⊨ T$$$

Lean4

instance theory_model {T : L.Theory} [h : M ⊨ T] {S : L.ElementarySubstructure M} : S ⊨ T :=
  (theory_model_iff S T).2 h

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

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

Разделы

Аффилиация

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