English
The age of a direct limit of structures is the union of the ages of the constituent structures.
Русский
Возраст прямого предела структур равен объединению возрастов составляющих структур.
LaTeX
$$$\mathrm{age}_L(\mathrm{DirectLimit} G f) = \bigcup_{i \in \iota} \mathrm{age}_L(G(i))$$$
Lean4
/-- The age of a countable structure is essentially countable (has countably many isomorphism
classes). -/
theorem countable_quotient [h : Countable M] : (Quotient.mk' '' L.age M).Countable := by
classical
refine
(congr_arg _ (Set.ext <| Quotient.forall.2 fun N => ?_)).mp
(countable_range fun s : Finset M => ⟦⟨closure L (s : Set M), inferInstance⟩⟧)
constructor
· rintro ⟨s, hs⟩
use Bundled.of (closure L (s : Set M))
exact ⟨⟨(fg_iff_structure_fg _).1 (fg_closure s.finite_toSet), ⟨Substructure.subtype _⟩⟩, hs⟩
· simp only [mem_range, Quotient.eq]
rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
exact
⟨PM.equivRange.symm⟩
-- This is not a simp-lemma because it does not apply to itself.
