English
If M and N are Fraïssé limits of the same class K, then they are isomorphic.
Русский
Если M и N являются пределами Фраиссe одного и того же класса K, то они изоморфны.
LaTeX
$$$IsFraisseLimit(K,M) \land IsFraisseLimit(K,N) \rightarrow \exists e:\ M \cong_L N$$$
Lean4
/-- The Fraïssé limit of a class is unique, in that any two Fraïssé limits are isomorphic. -/
theorem nonempty_equiv : Nonempty (M ≃[L] N) :=
by
let S : L.Substructure M := ⊥
have S_fg : FG L S := (fg_iff_structure_fg _).1 Substructure.fg_bot
obtain ⟨_, ⟨emb_S : S ↪[L] N⟩⟩ : ⟨S, inferInstance⟩ ∈ L.age N :=
by
rw [hN.age, ← hM.age]
exact ⟨S_fg, ⟨subtype _⟩⟩
let v : M ≃ₚ[L] N :=
{ dom := S
cod := emb_S.toHom.range
toEquiv := emb_S.equivRange }
exact
⟨Exists.choose
(equiv_between_cg cg_of_countable cg_of_countable ⟨v, ((Substructure.fg_iff_structure_fg _).2 S_fg)⟩
(hM.isExtensionPair hN) (hN.isExtensionPair hM))⟩
