countable_fg_substructures_of_countable

English

Let M be a countable L-structure. Then the collection of finitely generated substructures S of M is countable.

Русский

Пусть M — счётная L-структура. Тогда множество конечнопорождённых подструктур S внутри M счётно.

LaTeX

$$$\operatorname{Countable}\bigl\{ S : L\text{-Substructure } M \mid S.FG \bigr\}$$$

Lean4

theorem countable_fg_substructures_of_countable [Countable M] : Countable { S : L.Substructure M // S.FG } :=
  by
  let g : { S : L.Substructure M // S.FG } → Finset M := fun S ↦ Exists.choose S.prop
  have g_inj : Function.Injective g := by
    intro S S' h
    apply Subtype.eq
    rw [(Exists.choose_spec S.prop).symm, (Exists.choose_spec S'.prop).symm]
    exact congr_arg ((closure L) ∘ Finset.toSet) h
  exact Function.Embedding.countable ⟨g, g_inj⟩

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