cg_of_fg

Mathlib.ModelTheory.FinitelyGenerated

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

English

There is an instance cg_of_fg: FG L M implies CG L M.

Русский

Существует переход cg_of_fg: FG L M => CG L M.

LaTeX

$$$$ FG\\;L\\;M \\Rightarrow CG\\;L\\;M. $$$$

Lean4

instance (priority := 100) cg_of_fg [h : FG L M] : CG L M :=
  h.cg

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

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

Разделы

Аффилиация

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