models_of_isUniversal

Mathlib.ModelTheory.Complexity

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.models_of_isUniversal

← MathLib Explorer

English

If S is a substructure of M, and M ⊨ T with T universal, then S ⊨ T.

Русский

Пусть S — подструктура M; если M ⊨ T и T универсальна, то и S ⊨ T.

LaTeX

$$$S \subseteq M \; \Rightarrow \; (M ⊨ T) \Rightarrow (S ⊨ T)$$$

Lean4

instance models_of_isUniversal (S : L.Substructure M) (T : L.Theory) [T.IsUniversal] [M ⊨ T] : S ⊨ T :=
  Theory.IsUniversal.models_of_embedding (Substructure.subtype S)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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