countable_self_fgequiv_of_countable

English

If M is countable, then L.FGEquiv M M is countable.

Русский

Если M счетно, то L.FGEquiv M M счетно.

LaTeX

$$$[Countable M] : Countable (L.FGEquiv M M).$$$

Lean4

theorem countable_self_fgequiv_of_countable [Countable M] : Countable (L.FGEquiv M M) :=
  by
  let g : L.FGEquiv M M → Σ U : { S : L.Substructure M // S.FG }, U.val →[L] M := fun f ↦
    ⟨⟨f.val.dom, f.prop⟩, (subtype _).toHom.comp f.val.toEquiv.toHom⟩
  have g_inj : Function.Injective g := by
    intro f f' h
    ext
    let ⟨⟨dom_f, cod_f, equiv_f⟩, f_fin⟩ := f
    cases congr_arg (·.1) h
    apply PartialEquiv.ext (by rfl)
    simp only [g, Sigma.mk.inj_iff, heq_eq_eq, true_and] at h
    exact fun x hx ↦ congr_fun (congr_arg (↑) h) ⟨x, hx⟩
  have : ∀ U : { S : L.Substructure M // S.FG }, Structure.FG L U.val := fun U ↦ (U.val.fg_iff_structure_fg.1 U.prop)
  exact Function.Embedding.countable ⟨g, g_inj⟩

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