Commit 2024-09-09 16:04 23abd25c

feat(ModelTheory/Order): Countable dense linear orders are Fraïssé limits of the class of finite linear orders (#16538) FirstOrder.Language.IsExtensionPair_iff_exists_embedding_closure_singleton_sup is a characterization of FirstOrder.Language.IsExtensionPair in terms of extending the domain of an embedding. FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo shows that any countable nonempty model of the theory of linear orders is a Fraïssé limit of the class of finite models of the theory of linear orders. FirstOrder.Language.isFraisse_finite_linear_order shows that the class of finite models of the theory of linear orders is Fraïssé.