cg_of_countable

Mathlib.ModelTheory.FinitelyGenerated

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

English

If M is countable, then L cg M holds for any language L.

Русский

Если M счётно, то cg L M выполняется для любого языка L.

LaTeX

$$$$ [Countable M] \\Rightarrow CG\\;L\\;M.$$$$

Lean4

theorem cg_of_countable [Countable M] : CG L M := by simp only [cg_def, Substructure.cg_of_countable]

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

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

Разделы

Аффилиация

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