cg

Mathlib.ModelTheory.FinitelyGenerated

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Structure.FG.cg

English

If M is finitely generated, then the CG property holds for L-structures M.

Русский

Если M является порожденной сколь угодно компактно (FG), то cg для L-структуры M выполняется.

LaTeX

$$$$\n\\text{If } FG_L M, \\text{ then } CG_L M. \n$$$$

Lean4

theorem cg (h : FG L M) : CG L M :=
  cg_def.2 (fg_def.1 h).cg

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

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

Разделы

Аффилиация

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