cg_closure_singleton

Mathlib.ModelTheory.FinitelyGenerated

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

English

The closure of a singleton is CG.

Русский

Замыкание одиночного множества CG.

LaTeX

$$$CG(closure L ({ x } : Set M))$$$

Lean4

theorem cg_closure_singleton (x : M) : CG (closure L ({ x } : Set M)) :=
  (fg_closure_singleton x).cg

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

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

Разделы

Аффилиация

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