cg_closure

Mathlib.ModelTheory.FinitelyGenerated

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

English

If s is countable, then closure L s is CG.

Русский

Если s счётно, то closure_L(s) CG.

LaTeX

$$$s.Countable \Rightarrow CG(closure L s)$$$

Lean4

theorem cg_closure {s : Set M} (hs : s.Countable) : CG (closure L s) :=
  ⟨s, hs, rfl⟩

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

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

Разделы

Аффилиация

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