Strict total orders

StructureStrict total order#✓fully proved

A strict total order on a type \(\alpha\) consists of a binary relation \(<\) on \(\alpha\) that is irreflexive (no \(a < a\)), transitive (\(a < b\) and \(b < c\) imply \(a < c\)) and total on distinct elements (if \(a \ne b\), then \(a < b\) or \(b < a\)). It models strict preference.

structure StrictTotalOrder (α : Type*) where
  lt : α → α → Prop
  irrefl : ∀ a, ¬ lt a a
  trans : ∀ {a b c}, lt a b → lt b c → lt a c
  total : ∀ {a b}, a ≠ b → lt a b ∨ lt b a

Used by 33

Used byGale-Shapley serves every preference profile with \(n\) proposers and \(n\) receivers · Every strict total order on \(\{0, \dots, n-1\}\) is given by a ranking · Rank under a strict total order · Preference order of a ranking · Arrow's impossibility theorem for strict preferences, general form · Irreflexivity of strict preference (Arrow's theorem) · Preference relation of a strict total order (Arrow's theorem) · Strict total order from a relation (Arrow's theorem) · Strict preference orders for Arrow's theorem · Strict preference orders for Arrow's theorem are total · Strict preference orders for Arrow's theorem are transitive · Gibbard–Satterthwaite theorem, finiteness form · Irreflexivity of strict preference · Relation of a strict preference order · Building a strict preference order in the Gibbard–Satterthwaite setting · Strict preference orders for the Gibbard–Satterthwaite theorem · Strict preferences in the Gibbard–Satterthwaite setting are total · Transitivity of strict preferences in the Gibbard–Satterthwaite setting · Order-robust ordered Ramsey conjecture for 100-regular graphs · Blue ordered copy · Red ordered copy · Ordered embedding · Ordered Ramsey number · Ordered Ramsey property · Irreflexivity of a strict total order · Relation of a strict total order · Men's preferences induced by rankings · Building a strict total order from a relation · Strict preference order · Strict total orders are total on distinct elements · Transitivity of a strict total order · Women's preference orders of a profile · Strict total orders are determined by their relation

TheoremStrict total orders are determined by their relation#✓fully proved

Two strict total orders on a type \(\alpha\) with the same relation are equal.

@[ext]
theorem StrictTotalOrder.ext {α : Type*} {T T' : StrictTotalOrder α} (h : T.lt = T'.lt) :
    T = T'

Uses 1 · Used by 2

Statement usesStrict total order

Used byEvery strict total order on \(\{0, \dots, n-1\}\) is given by a ranking · Strict total orders are determined by their relation

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.