has_representative_as_substructure

English

Every class in the age of M has a representative that is a finitely generated substructure.

Русский

Каждый класс в возрасте M имеет представителя, который является FG-подструктурой.

LaTeX

$$Has_representative_as_substructure$$

Lean4

/-- Any class in the age of a structure has a representative which is a finitely generated
substructure. -/
theorem has_representative_as_substructure :
    ∀ C ∈ Quotient.mk' '' L.age M, ∃ V : { V : L.Substructure M // FG V }, ⟦Bundled.mk V⟧ = C :=
  by
  rintro _ ⟨N, ⟨N_fg, ⟨N_incl⟩⟩, N_eq⟩
  refine N_eq.symm ▸ ⟨⟨N_incl.toHom.range, ?_⟩, Quotient.sound ⟨N_incl.equivRange.symm⟩⟩
  exact FG.range N_fg (Embedding.toHom N_incl)

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