Theorems · Theorem · logic and foundations

FirstOrder.Language.Term.realize_lt

∀ {L : FirstOrder.Language} {α : Type w} {M : Type w'} {n : ℕ} [inst : L.IsOrdered] [inst_1 : L.Structure M]
  [inst_2 : Preorder M] [L.OrderedStructure M] {t₁ t₂ : L.Term (α ⊕ Fin n)} {v : α → M} {xs : Fin n → M},
  (t₁.lt t₂).Realize v xs ↔
    FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ < FirstOrder.Language.Term.realize (Sum.elim v xs) t₂

Defined in

Mathlib.ModelTheory.Order

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.IsOrderedFirstOrder.Language.StructurePreorderFirstOrder.Language.OrderedStructure