isFraisseLimit_of_countable_nonempty_dlo

English

Any countable nonempty dense linear order is the Fraïssé limit of finite linear orders.

Русский

Любой счетный непустой плотный линейный порядок является пределом Фрайсе множества конечных линейных порядков.

LaTeX

$$$ \text{IsFraisseLimit} \big( \{ M \mid \ Finite(M) \land M \models \text{linearOrderTheory} \} \big) M $$$

Lean4

/-- Any countable nonempty model of the theory of dense linear orders is a Fraïssé limit of the
class of finite models of the theory of linear orders. -/
theorem isFraisseLimit_of_countable_nonempty_dlo (M : Type w) [Language.order.Structure M] [Countable M] [Nonempty M]
    [M ⊨ Language.order.dlo] :
    IsFraisseLimit
      {M : CategoryTheory.Bundled.{w} Language.order.Structure | Finite M ∧ M ⊨ Language.order.linearOrderTheory} M :=
  ⟨(isUltrahomogeneous_iff_IsExtensionPair cg_of_countable).2 (dlo_isExtensionPair M M), dlo_age M⟩

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