Theorems · Definition · logic and foundations

FirstOrder.Language.Term.lt

{L : FirstOrder.Language} →
  {α : Type w} → {n : ℕ} → [L.IsOrdered] → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin n) → L.BoundedFormula α n

Joins two terms t₁, t₂ in a formula representing t₁ < t₂.

Defined in

Mathlib.ModelTheory.Order

Cited by

1 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext

Assumes

FirstOrder.Language.IsOrdered