English
Characterizes when K is the age of a countably generated structure in terms of countability and embedding properties.
Русский
Характеризует, когда K является возрастом счетно порождаемой структуры в терминах счётности и вложений.
LaTeX
$$(Exists fun M => Countable M ∧ L.age M = K) ↔ (K.Nonempty ∧ (∀ M N, Nonempty (M ≃ N) → (M ∈ K ↔ N ∈ K)) ∧ (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, FG L M) ∧ Hereditary K ∧ JointEmbedding K)$$
Lean4
theorem exists_countable_is_age_of_iff [Countable (Σ l, L.Functions l)] :
(∃ M : Bundled.{w} L.Structure, Countable M ∧ L.age M = K) ↔
K.Nonempty ∧
(∀ M N : Bundled.{w} L.Structure, Nonempty (M ≃[L] N) → (M ∈ K ↔ N ∈ K)) ∧
(Quotient.mk' '' K).Countable ∧
(∀ M : Bundled.{w} L.Structure, M ∈ K → Structure.FG L M) ∧ Hereditary K ∧ JointEmbedding K :=
by
constructor
· rintro ⟨M, h1, h2, rfl⟩
refine
⟨age.nonempty M, age.is_equiv_invariant L M, age.countable_quotient M, fun N hN => hN.1, age.hereditary M,
age.jointEmbedding M⟩
· rintro ⟨Kn, _, cq, hfg, hp, jep⟩
obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn cq hfg hp jep
exact ⟨M, Structure.cg_iff_countable.1 hM, rfl⟩
