fg_closure_singleton

Mathlib.ModelTheory.FinitelyGenerated

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

English

The closure of a singleton is finitely generated.

Русский

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

LaTeX

$$$FG(closure_L(\{x\}))$$$

Lean4

theorem fg_closure_singleton (x : M) : FG (closure L ({ x } : Set M)) :=
  fg_closure (finite_singleton x)

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

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

Разделы

Аффилиация

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