of_small

Mathlib.ModelTheory.Bundled

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

English

If M is a model of T and T' ⊆ T, then M with the subtheory structure is a model of T'.

Русский

Если M — модель T, и T' ⊆ T, то модель M с учётом подтеории T' удовлетворяет T'.

LaTeX

$$$M.\text{subtheoryModel } h \vDash T' \quad\text{whenever } h: T' \subseteq T$$$

Lean4

instance of_small (M : Type w) [Nonempty M] [L.Structure M] [M ⊨ T] [h : Small.{w'} M] :
    Small.{w'} (ModelType.of T M) :=
  h

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

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

Разделы

Аффилиация

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