English
The Fraïssé limit of the class of finite L-empty-structure is M, i.e., IsFraisseLimit of finite L-empty-structures holding for M.
Русский
Предел Фраиссe класса конечных структур пустого языка существует и даёт структуру M; то есть IsFraisseLimit для конечных структур пустого языка верно для M.
LaTeX
$$$IsFraisseLimit(\{S : Bundled(Language.empty.Structure) \mid Finite S\}, M)$$$
Lean4
/-- Any countable infinite structure in the empty language is a Fraïssé limit of the class of finite
structures. -/
theorem isFraisseLimit_of_countable_infinite (M : Type*) [Countable M] [Infinite M] [Language.empty.Structure M] :
IsFraisseLimit {S : Bundled Language.empty.Structure | Finite S} M
where
age := by
ext S
simp only [age, Structure.fg_iff_finite, mem_setOf_eq, and_iff_left_iff_imp]
intro hS
simp
ultrahomogeneous S hS
f := by
classical
have : Finite S := hS.finite
have : Infinite { x // x ∉ S } := ((Set.toFinite _).infinite_compl).to_subtype
have : Finite f.toHom.range := (((Substructure.fg_iff_structure_fg S).1 hS).range _).finite
have : Infinite { x // x ∉ f.toHom.range } := ((Set.toFinite _).infinite_compl).to_subtype
refine ⟨StrongHomClass.toEquiv (f.equivRange.subtypeCongr nonempty_equiv_of_countable.some), ?_⟩
ext x
simp [Equiv.subtypeCongr]
