`<`

for less than was defined in [[Interface:First-order linear order defined via strict inequality]], which also provides the builder `LessThanBuilder`

, transitivity, asymmetry, and totality. We add some consequences and convenience theorems.
#
# We also provide greater-than, which is just an abbreviation for less-than with the order of the arguments reversed.
term (formula (> x y))
stmt (GreaterThan () () (↔ (> x y) (< y x)))
#
# === Trichotomy ===
# Exactly one of `x < y`

, `x = y`

, or `y < x`

hold. Our propositional logic doesn't have a notation which directly states "exactly one of three propositions holds" and even if it did, it might be inconvenient to work with. So we provide multiple theorems to express this idea.
stmt (LessThanEquality () () (→ (< x y) (¬ (= x y))))
stmt (LessThanGreaterThan () () (→ (< x y) (¬ (> x y))))
stmt (EqualityLessThan () () (→ (= x y) (¬ (< x y))))
#
# == Less than or equal to ==
# There is a predicate for less than or equal to.
term (formula (≤ x y))
#
# It is transitive, antisymmetric, and total.
stmt (LessEqualTransitivity () () (→ (∧ (≤ x y) (≤ y z)) (≤ x z)))
stmt (LessEqualAntisymmetry () () (→ (∧ (≤ x y) (≤ y x)) (= x y)))
stmt (LessEqualTotality () () (∨ (≤ x y) (≤ y x)))
#
# One consequence is reflexivity.
stmt (LessEqualReflexivity () () (≤ x x))
#
# We also provide greater-than-or-equal, which is just an abbreviation for less-than-or-equal with the order of the arguments reversed.
term (formula (≥ x y))
stmt (GreaterEqual () () (↔ (≥ x y) (≤ y x)))
#
# == Relationships between less-than, less-equal, and equality ==
stmt (LessThanLessEqual () () (↔ (< x y) (∧ (≤ x y) (¬ (= x y)))))
stmt (LessEqualLessThan () () (↔ (≤ x y) (∨ (< x y) (= x y))))
stmt (LessThanLessEqualImplication () () (→ (< x y) (≤ x y)))
stmt (EqualityLessEqual () () (→ (= x y) (≤ x y)))
stmt (LessEqualLessThanTransitivity () () (→ (∧ (≤ x y) (< y z)) (< x z)))
#
# == Builders ==
# Both predicates obey the usual builders. `LessEqualBuilder`

was already defined, so it is the only one not defined here.
stmt (LessThanBuilderLL () () (→ (= y0 y1) (↔ (< x y0) (< x y1))))
stmt (LessThanBuilderRR () () (→ (= x0 x1) (↔ (< x0 y) (< x1 y))))
stmt (buildLessThan () ((= x0 x1) (= y0 y1)) (↔ (< x0 y0) (< x1 y1)))
stmt (buildLessThanLL () ((= y0 y1)) (↔ (< x y0) (< x y1)))
stmt (buildLessThanRR () ((= x0 x1)) (↔ (< x0 y) (< x1 y)))
stmt (LessEqualBuilderRR () () (→ (= x0 x1) (↔ (≤ x0 y) (≤ x1 y))))
stmt (LessEqualBuilderLL () () (→ (= y0 y1) (↔ (≤ x y0) (≤ x y1))))
stmt (LessEqualBuilder () () (→ (∧ (= x0 x1) (= y0 y1)) (↔ (≤ x0 y0) (≤ x1 y1))))
stmt (buildLessEqual () ((= x0 x1) (= y0 y1)) (↔ (≤ x0 y0) (≤ x1 y1)))
stmt (buildLessEqualRR () ((= x0 x1)) (↔ (≤ x0 y) (≤ x1 y)))
stmt (buildLessEqualLL () ((= y0 y1)) (↔ (≤ x y0) (≤ x y1)))
#
# {{DEFAULTSORT:{{PAGENAME}}}}
# [[Category:Total order]]