isFraisse_finite_linear_order — Mathlib

English

The class of finite models of the theory of linear orders is Fraïssé.

Русский

Класс конечных моделей теории линейных порядков является Фрайсе.

LaTeX

$$$ \text{IsFraisse } \{M : \text{Bundled }\text{Language.order.Structure} \mid Finite M \land M \models \text{linearOrderTheory} \} $$$

Lean4

/-- The class of finite models of the theory of linear orders is Fraïssé. -/
theorem isFraisse_finite_linear_order :
    IsFraisse
      {M : CategoryTheory.Bundled.{0} Language.order.Structure | Finite M ∧ M ⊨ Language.order.linearOrderTheory} :=
  by
  letI : Language.order.Structure ℚ := orderStructure _
  exact (isFraisseLimit_of_countable_nonempty_dlo ℚ).isFraisse

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