Theorems · Definition · logic and foundations

FirstOrder.Language.decidableLEOfStructure

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

The order structure on an ordered language is decidable.

Defined in

Mathlib.ModelTheory.Order

Cited by

0 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext

Assumes

FirstOrder.Language.IsOrderedFirstOrder.Language.StructureDecidableRel