instCountable_embedding

Mathlib.ModelTheory.FinitelyGenerated

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

English

If L M is finitely generated (CG), then there exists a corresponding CG structure.

Русский

Если L-структура M конечнопорождена, то существует связанная CG-структура.

LaTeX

$$$\text{CG}(L,M) \Rightarrow \text{FG}(L,M)$$$

Lean4

instance instCountable_embedding (N : Type*) [L.Structure N] [Countable N] [h : FG L M] : Countable (M ↪[L] N) :=
  FG.countable_embedding N h

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

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

Разделы

Аффилиация

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