English
The age of a countable M has a countable quotient of isomorphism classes.
Русский
Возраст счётной M имеет счётный фактор изоморфизмов классов.
LaTeX
$$[h : Countable M] : (Quotient.mk' '' L.age M).Countable$$
Lean4
/-- The age of a direct limit of structures is the union of the ages of the structures. -/
theorem age_directLimit {ι : Type w} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι] (G : ι → Type max w w')
[∀ i, L.Structure (G i)] (f : ∀ i j, i ≤ j → G i ↪[L] G j) [DirectedSystem G fun i j h => f i j h] :
L.age (DirectLimit G f) = ⋃ i : ι, L.age (G i) := by
classical
ext M
simp only [mem_iUnion]
constructor
· rintro ⟨Mfg, ⟨e⟩⟩
obtain ⟨s, hs⟩ := Mfg.range e.toHom
let out := @Quotient.out _ (DirectLimit.setoid G f)
obtain ⟨i, hi⟩ := Finset.exists_le (s.image (Sigma.fst ∘ out))
have e' := (DirectLimit.of L ι G f i).equivRange.symm.toEmbedding
refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩
rw [← hs, closure_le]
intro x hx
refine ⟨f (out x).1 i (hi (out x).1 (Finset.mem_image_of_mem _ hx)) (out x).2, ?_⟩
rw [Embedding.coe_toHom, DirectLimit.of_apply, @Quotient.mk_eq_iff_out _ (_),
DirectLimit.equiv_iff G f (le_refl _) (hi (out x).1 (Finset.mem_image_of_mem _ hx)), DirectedSystem.map_self]
· rintro ⟨i, Mfg, ⟨e⟩⟩
exact ⟨Mfg, ⟨Embedding.comp (DirectLimit.of L ι G f i) e⟩⟩
