instCountable_fg_substructures_of_countable

English

If M is a countable L-structure, then the collection of finitely generated L-substructures of M is countable.

Русский

Если M является счётной L-структурой, то множество конечносгенерированных подструктур M в языке L счётно.

LaTeX

$$$\operatorname{Countable}\{ S : L.Substructure M \mid S.FG \}$$$

Lean4

instance instCountable_fg_substructures_of_countable [Countable M] : Countable { S : L.Substructure M // S.FG } :=
  countable_fg_substructures_of_countable

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