cg_def

Mathlib.ModelTheory.FinitelyGenerated

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

English

CG L M is equivalent to (⊤).CG via the top substructure.

Русский

CG L M эквивалентно CG верхней подпструктуры ⊤.

LaTeX

$$$\text{CG}(L,M) \iff \big(\top : L.Substructure M\big).CG$$$

Lean4

theorem cg_def : CG L M ↔ (⊤ : L.Substructure M).CG :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

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

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

Разделы

Аффилиация

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