Theorems · Theorem · logic and foundations

FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo

∀ (M : Type w) [inst : FirstOrder.Language.order.Structure M] [inst_1 : Countable M] [Nonempty M]
  [M ⊨ FirstOrder.Language.order.dlo],
  FirstOrder.Language.IsFraisseLimit {M | Finite ↑M ∧ ↑M ⊨ FirstOrder.Language.order.linearOrderTheory} M

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.

Defined in

Mathlib.ModelTheory.Order

Cited by

2 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureCountableNonemptyFirstOrder.Language.Theory.Model