fg_closure

Mathlib.ModelTheory.FinitelyGenerated

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

English

If s is finite, then closure_L(s) is finitely generated.

Русский

Если s конечно, то closure_L(s) конечно порождаемое.

LaTeX

$$$s\text{ finite} \Rightarrow FG(closure_L\,s)$$$

Lean4

theorem fg_closure {s : Set M} (hs : s.Finite) : FG (closure L s) :=
  ⟨hs.toFinset, by rw [hs.coe_toFinset]⟩

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

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

Разделы

Аффилиация

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