fg_iff_finite

Mathlib.ModelTheory.FinitelyGenerated

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

English

Under relational L.IsRelational, FG L M is equivalent to Finite M.

Русский

При реляционности L.IsRelational FG L M эквивалентно Finite M.

LaTeX

$$$[L.IsRelational] \Rightarrow (\text{FG } L M \iff \text{Finite } M)$$$

Lean4

theorem fg_iff_finite [L.IsRelational] : FG L M ↔ Finite M :=
  ⟨FG.finite, fun _ => FG.of_finite⟩

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

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

Разделы

Аффилиация

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