age_isFraisse — Mathlib

English

If M is ultrahomogeneous, the amalgamation property for its age implies that the age is Fraisse.

Русский

Если M ультрахомогенна, амальгамирование возраста порождает Fraisse-возраст.

LaTeX

$$amalgamation_age ⇒ IsFraisse (L.age M)$$

Lean4

theorem age_isFraisse [Countable M] (h : L.IsUltrahomogeneous M) : IsFraisse (L.age M) :=
  ⟨age.nonempty M, fun _ hN => hN.1, age.countable_quotient M, age.hereditary M, age.jointEmbedding M,
    h.amalgamation_age⟩

Похожие утверждения