Theorems · Definition · logic and foundations

FirstOrder.Language.linearOrderOfModels

(L : FirstOrder.Language) →
  (M : Type w') →
    [inst : L.IsOrdered] →
      [inst_1 : L.Structure M] →
        [h : M ⊨ L.linearOrderTheory] →
          [DecidableRel fun a b => FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b]] →
            LinearOrder M

Any model of a theory of linear orders is a linear order.

Defined in

Mathlib.ModelTheory.Order

Cited by

2 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.IsOrderedFirstOrder.Language.StructureFirstOrder.Language.Theory.ModelDecidableRel