finite

Mathlib.ModelTheory.FinitelyGenerated

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

English

CG L M is equivalent to top.CG.

Русский

CG L M эквивалентно top.CG.

LaTeX

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

Lean4

theorem finite [L.IsRelational] (h : FG L M) : Finite M :=
  Finite.of_finite_univ (Substructure.FG.finite (fg_def.1 h))

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

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

Разделы

Аффилиация

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