Orders, lattices and well-orders

Lens

MotivationH

Which phone is best?

A student in Accra is choosing a phone. She cares about two things: price (lower is better) and battery life (longer is better).

Phone	Price (cedis)	Battery (hours)
A	1 200	20
B	1 500	30
C	1 800	25
D	2 400	40
E	1 400	18

Phone B is better than C in both respects, and A is better than E. But A and B cannot be compared: A is cheaper, B lasts longer. So "is at least as good in both respects as" orders the phones only partially. There is no single best phone; instead there are several that nothing beats — A, B and D — which economists call Pareto optimal, after the Italian economist Vilfredo Pareto, and mathematicians call maximal.

Partial orders are everywhere once you look: train and coach journeys from Osaka to Tokyo compared by fare and travel time (the bullet train is fastest, the overnight coach is cheapest, and neither beats the other), courses and their prerequisites (this curriculum is organised by one), tasks in a building project, versions of a document, subsets ordered by inclusion, whole numbers ordered by divisibility. This lesson gives the precise language for them — and shows how carefully one must use words like "best", "bound" and "least" when not everything can be compared.

IntuitionH

Pictures of orders: Hasse diagrams

A finite partial order can be drawn as a Hasse diagram: put larger elements higher up, and draw a line from $a$ up to $b$ when $b$ covers $a$ — that is, $a < b$ with nothing strictly in between. All other comparisons are then read off as upward paths: $a \le b$ exactly when one can climb from $a$ to $b$ .

Here are the subsets of $\{1, 2, 3\}$ ordered by inclusion. The diagram is a cube: $\varnothing$ at the bottom, the whole set at the top.

(\mathcal{P}(\{1, 2, 3\}), \subseteq)

. Arrows go from a set to the sets covering it.

\{1\}

and

\{2, 3\}

are incomparable.

And here is divisibility on $\{1, \dots, 12\}$ , with $a$ below $b$ when $a \mid b$ . Try tracing upward walks: each one is a chain, a set of pairwise comparable elements. Notice how many elements sit at the top with nothing above them.

Divisibility on {1, …, 12}

Edges join a number to the multiples that cover it. Which numbers have nothing above them?

|V| = 12|E| = 14Click edges one after another to walk along them, or pick a starting vertex first.

No walk yet.

8 vertices have odd degree: 1, 3, 7, 11, 4, 6, 9, 8.

So no Euler trail is possible. A trail enters and leaves each vertex in its middle in pairs, so only its two ends can have odd degree, and this graph has 8 such vertices.

DefinitionsH

Definitions

Definition— preorder, partial order, total order

A relation $\le$ on a set $P$ is a preorder if it is reflexive ( $a \le a$ ) and transitive ( $a \le b$ and $b \le c$ imply $a \le c$ ). It is a partial order if moreover it is antisymmetric ( $a \le b$ and $b \le a$ imply $a = b$ ); then $(P, \le)$ is a partially ordered set, or poset. Elements with $a \le b$ or $b \le a$ are comparable. A partial order in which every two elements are comparable is a total (or linear) order. We write $a < b$ for " $a \le b$ and $a \neq b$ ".

Definition— chain, antichain, cover

A chain is a subset in which every two elements are comparable; an antichain is one in which no two distinct elements are. $b$ covers $a$ if $a < b$ and there is no $c$ with $a < c < b$ ; the covering pairs are the edges of the Hasse diagram.

Definition— maximal and greatest elements

An element $m \in P$ is maximal if there is no $x \in P$ with $m < x$ , and greatest if $x \le m$ for every $x \in P$ . Minimal and least elements are defined dually.

Definition— upper bounds and suprema

Let $S \subseteq P$ . An upper bound of $S$ is an element $b \in P$ with $s \le b$ for all $s \in S$ . A least upper bound or supremum of $S$ , written $\sup S$ or $\bigvee S$ , is an upper bound that is $\le$ every upper bound. Lower bounds and the greatest lower bound (infimum, $\inf S$ or $\bigwedge S$ ) are defined dually. Note that $\sup S$ is an element of $P$ ; it need not belong to $S$ .

Definition— lattice, complete lattice

A lattice is a poset in which every pair $a, b$ has a supremum $a \vee b$ (the join) and an infimum $a \wedge b$ (the meet). A complete lattice is a poset in which every subset, including $\varnothing$ and infinite ones, has a supremum and an infimum.

Definition— well-order

A well-order is a total order in which every non-empty subset has a least element.

Definition— monotone map

A map $f : P \to Q$ between posets is monotone (order-preserving) if $a \le b$ implies $f(a) \le f(b)$ . A fixed point of $f : P \to P$ is an element with $f(a) = a$ .

Definition— Zorn's lemma

Zorn's lemma: if $P$ is a non-empty poset in which every chain has an upper bound in $P$ , then $P$ has a maximal element. (We state it now and discuss its status below.)

Worked examplesH

Examples and non-examples

Example— Orders on numbers

$(\N, \le)$ , $(\Z, \le)$ , $(\Q, \le)$ and $(\R, \le)$ are total orders.
$(\N, \mid)$ , divisibility, is a partial order but not a total one ( $2$ and $3$ are incomparable). Its least element is $1$ , which divides everything; its greatest element is $0$ , which every number divides.
On $\Z$ , divisibility is only a preorder: $2 \mid -2$ and $-2 \mid 2$ but $2 \neq -2$ . Identifying each integer with its negative (passing to equivalence classes) turns it into a partial order — a general way of making a preorder into a partial order.
The strict relation $<$ is not a partial order in our sense, because it is not reflexive; it is a strict order. Partial orders and strict orders correspond one-to-one via $a < b \iff (a \le b$ and $a \neq b)$ .

Example— Orders on pairs

On $\R^2$ , the product order $(a, b) \le (c, d) \iff a \le c$ and $b \le d$ is partial: $(1, 2)$ and $(2, 1)$ are incomparable. This is the Pareto order of the motivating example, with prices negated. The lexicographic order — compare first coordinates, and use the second only to break ties, as in a dictionary — is total.

Example— Maximal but not greatest

In $(\{1, \dots, 12\}, \mid)$ the maximal elements are $7, 8, 9, 10, 11, 12$ — exactly the numbers with no proper multiple in the set — and there is no greatest element. The least element is $1$ . In the phones example, A, B and D are maximal and none is greatest.

Example— Bounds and suprema

In $(\mathcal{P}(A), \subseteq)$ , every family of subsets has a supremum, its union, and an infimum, its intersection: $\mathcal{P}(A)$ is a complete lattice.
In $(\N, \mid)$ , $\gcd(a, b)$ is the meet of $a$ and $b$ and $\operatorname{lcm}(a, b)$ is the join; $(\N, \mid)$ is a lattice (in fact a complete one). But $\{1, \dots, 12\}$ with divisibility is not a lattice: $2$ and $7$ have no upper bound in the set at all.
In $(\Q, \le)$ , the set $\{q : q < 1\}$ has supremum $1$ , which is not in the set, while $\{q : q^2 < 2\}$ is bounded above but has no supremum in $\Q$ (see real numbers).

ProofH

Maximal elements and suprema

Theorem— Proposition 1 (greatest versus maximal)

In a poset, a greatest element, if it exists, is unique and is the only maximal element. In a total order, an element is maximal if and only if it is greatest.

Proof

If $g$ and $g'$ are greatest, then $g \le g'$ and $g' \le g$ , so $g = g'$ by antisymmetry. A greatest $g$ is maximal: if $g < x$ then also $x \le g$ , and antisymmetry gives $x = g$ , contradicting $g < x$ . If $m$ is any maximal element, then $m \le g$ , and maximality forbids $m < g$ , so $m = g$ . In a total order, let $m$ be maximal and $x$ arbitrary; $x$ and $m$ are comparable, and $m < x$ is impossible, so $x \le m$ : $m$ is greatest.

∎

Theorem— Theorem 2 (finite posets have maximal elements)

Every finite non-empty poset has a maximal element.

Proof

First proof (climbing). Start at any element $a_0$ . If it is not maximal, pick $a_1 > a_0$ ; if $a_1$ is not maximal, pick $a_2 > a_1$ , and so on. By transitivity $a_i < a_j$ whenever $i < j$ , so the $a_i$ are distinct (if $a_i = a_j$ with $i < j$ we would have $a_i < a_i$ ). A finite set cannot contain infinitely many distinct elements, so the climb stops — at a maximal element.

Second proof (counting, the one checked in Lean). For each $y$ let $D(y) = \{x : x \le y\}$ be its down-set, and choose $m$ with $|D(m)|$ as large as possible. If $m \le x$ , then $D(m) \subseteq D(x)$ by transitivity; by the choice of $m$ , $|D(x)| \le |D(m)|$ , so $D(m) = D(x)$ . As $x \in D(x) = D(m)$ , we get $x \le m$ , and antisymmetry gives $x = m$ . So nothing is strictly above $m$ .

∎

The first proof makes a sequence of choices, which is harmless for finitely many steps; for infinite posets the climb may go on for ever ( $0 < 1 < 2 < \cdots$ in $\N$ ), and Zorn's lemma is exactly the principle that rescues it when every chain is bounded.

Theorem— Corollary 3 (linear extensions)

Every partial order on a finite set can be extended to a total order: there is a total order $\preceq$ with $a \le b \Rightarrow a \preceq b$ .

Proof

Induction on the number of elements. The empty poset is totally ordered. Otherwise let $m$ be maximal (Theorem 2), totally order $P \setminus \{m\}$ extending its partial order (induction hypothesis), and put $m$ at the end. Since nothing in $P$ is strictly above $m$ , no comparison $m < x$ is violated.

∎

This is the mathematics behind topological sorting: listing courses so that every course comes after its prerequisites, or scheduling tasks so that each starts after the tasks it depends on.

Theorem— Proposition 4 (suprema are unique; unions and gcds)

A subset has at most one supremum. In $(\mathcal{P}(A), \subseteq)$ , $\sup\{S, T\} = S \cup T$ and $\inf\{S, T\} = S \cap T$ ; in $(\N, \mid)$ , $\inf\{a, b\} = \gcd(a, b)$ and $\sup\{a, b\} = \operatorname{lcm}(a, b)$ .

Proof

If $s$ and $s'$ are both suprema, each is an upper bound and each is below every upper bound, so $s \le s'$ and $s' \le s$ : $s = s'$ .

$S \cup T$ contains $S$ and $T$ , and any set $U$ containing both contains $S \cup T$ ; so $S \cup T$ is the least upper bound. Dually for $S \cap T$ . In $(\N, \mid)$ , $\gcd(a, b)$ divides $a$ and $b$ , and every common divisor of $a$ and $b$ divides $\gcd(a, b)$ (a consequence of Bézout's identity; see divisibility), so $\gcd(a, b)$ is the greatest lower bound in the divisibility order. Dually, every common multiple is a multiple of $\operatorname{lcm}(a, b)$ .

∎

In any lattice the operations satisfy associative and commutative laws, $a \vee a = a$ , and the absorption laws

a \vee (a \wedge b) = a, \qquad a \wedge (a \vee b) = a.

(For the first: $a$ is an upper bound of $a$ and of $a \wedge b \le a$ , so $a \vee (a \wedge b) \le a$ , and the reverse inequality always holds.) Conversely, a set with two operations obeying these laws is a lattice, ordered by $a \le b \iff a \wedge b = a$ : lattices can be defined algebraically, as in algebraic structures.

ProofH

Well-orders

Theorem— Theorem 5 (ℕ is well-ordered)

Every non-empty subset of $\N$ has a least element.

Proof

Suppose $S \subseteq \N$ has no least element. We show by strong induction that no $k$ lies in $S$ . Assume that no $n < k$ lies in $S$ . If $k \in S$ , then — as $k$ is not the least element of $S$ — some $n \in S$ satisfies $n < k$ , contradicting the assumption. So $k \notin S$ . Hence $S = \varnothing$ .

∎

The well-ordering principle and induction are two faces of the same fact (see proof techniques): induction can also be derived from well-ordering, by considering the least counterexample.

Theorem— Proposition 6 (ℤ and ℚ are not well-ordered)

$(\Z, \le)$ is not a well-order: $\Z$ itself has no least element. $(\Q, \le)$ is not a well-order either, and even $\{q \in \Q : q > 0\}$ has no least element.

Proof

For every $m \in \Z$ , $m - 1 < m$ . For every positive rational $m$ , $m/2$ is a smaller positive rational.

∎

Being well-ordered depends on the order, not just the set: $\Z$ can be well-ordered, for example as $0, -1, 1, -2, 2, \dots$ (compare by absolute value, negatives first). Cantor's ordinal numbers are the "lengths" of well-orders, continuing the natural numbers into the infinite: $0, 1, 2, \dots, \omega, \omega + 1, \dots$ Every well-order supports proofs by transfinite induction, the same argument as Theorem 5. Zermelo's well-ordering theorem (1904) says every set can be well-ordered — even $\R$ — but its proof uses the axiom of choice, and no explicit well-order of $\R$ can be written down.

ProofH

Fixed points and Zorn's lemma

Theorem— Theorem 7 (Knaster–Tarski)

Let $L$ be a complete lattice and $f : L \to L$ a monotone map. Then $f$ has a least fixed point, namely

a = \inf\{x \in L : f(x) \le x\}.

Proof

Let $X = \{x : f(x) \le x\}$ . For every $x \in X$ we have $a \le x$ , so $f(a) \le f(x) \le x$ by monotonicity. Thus $f(a)$ is a lower bound of $X$ , and $f(a) \le a$ since $a$ is the greatest lower bound. Applying $f$ , $f(f(a)) \le f(a)$ , so $f(a) \in X$ , and therefore $a \le f(a)$ . Hence $f(a) = a$ . Any fixed point $b$ satisfies $f(b) \le b$ , so $b \in X$ and $a \le b$ .

∎

This theorem is how mathematics and computer science define things "inductively". For instance, the set of vertices reachable from a vertex $v_0$ in a graph is the least fixed point of the monotone map $S \mapsto \{v_0\} \cup \{\text{successors of } S\}$ on the complete lattice of sets of vertices. In a finite lattice it can also be computed by iterating $f$ from the bottom element, $\varnothing \subseteq f(\varnothing) \subseteq f(f(\varnothing)) \subseteq \cdots$ , until the sequence stops growing. Knaster–Tarski also gives a slick proof of the Cantor–Schröder–Bernstein theorem (see cardinals).

Zorn's lemma. Theorem 2 guarantees maximal elements in finite posets. In infinite posets they may not exist — $(\N, \le)$ has none — and Zorn's lemma gives a sufficient condition: if every chain has an upper bound, a maximal element exists. It is the standard tool for producing "maximal" objects in infinite settings. For example, to find a basis of a vector space $V$ , consider the poset of linearly independent subsets of $V$ ordered by inclusion; the union of a chain of independent sets is independent and is an upper bound, so Zorn's lemma gives a maximal independent set, which must span $V$ (otherwise a vector outside the span could be added). The same pattern gives maximal ideals in rings. Zorn's lemma cannot be proved from the other axioms of set theory (ZF): over ZF it is equivalent to the axiom of choice (see the axiom of choice). In this lesson we use it as a tool, to be justified there.

Formal mathematicsF

Orders in Lean and Mathlib

Mathlib's order theory is organised by type classes — Preorder, PartialOrder, LinearOrder, Lattice (with ⊔ and ⊓), CompleteLattice (with sSup and sInf) — and predicates such as IsLUB s a ("a is a least upper bound of s") and IsMax m ("nothing is strictly above m").

Divisibility. Antisymmetry on $\N$ by the human argument ( $b = ak$ , $a = a(kl)$ , so $kl = 1$ ); a copy of $\N$ carrying the divisibility order, built as a genuine PartialOrder instance from the three axioms; and the failure of antisymmetry on $\Z$ .

nat_dvd_antisymmLean 4Proved here from basic factsFormally verified

/-- **Antisymmetry of divisibility on ℕ.** If `a ∣ b` and `b ∣ a` then `a = b`. Write `b = ak` and
`a = bl = a(kl)`. If `a = 0` then `b = 0` too; otherwise cancel `a` to get `kl = 1`, so `k = 1`
and `b = a`. (Reflexivity, `a ∣ a`, and transitivity are immediate.) -/
theorem nat_dvd_antisymm {a b : ℕ} (h₁ : a ∣ b) (h₂ : b ∣ a) : a = b := by
  obtain ⟨k, rfl⟩ := h₁
  obtain ⟨l, hl⟩ := h₂
  rcases Nat.eq_zero_or_pos a with rfl | ha
  · simp
  · have hkl : k * l = 1 := by
      have h : a * 1 = a * (k * l) := by rw [mul_one, ← mul_assoc]; exact hl
      exact (Nat.eq_of_mul_eq_mul_left ha h).symm
    rw [Nat.eq_one_of_mul_eq_one_right hkl, mul_one]

Axioms used: propextformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

DivNatLean 4Formally verified

/-- A copy of `ℕ` ordered by divisibility (`a ≤ b` means `a ∣ b`), so that Mathlib's order
library can be used on it. The axioms are `dvd_refl`, `dvd_trans` and `nat_dvd_antisymm`. In this
order `1` is the least element and `0` the greatest (every number divides `0`). -/
def DivNat : Type := ℕ

Axioms used: No axiomsformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

instPartialOrderLean 4Formally verified

/-- The partial order on `DivNat`. -/
instance DivNat.instPartialOrder : PartialOrder DivNat where
  le a b := @Dvd.dvd ℕ _ a b
  le_refl a := @dvd_refl ℕ _ a
  le_trans a b c := @dvd_trans ℕ _ a b c
  le_antisymm a b := @nat_dvd_antisymm a b

Axioms used: propextformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

int_dvd_not_antisymmLean 4Proved here from basic factsFormally verified

/-- **On ℤ, divisibility is only a preorder.** `2 ∣ -2` and `-2 ∣ 2`, yet `2 ≠ -2`:
antisymmetry fails because `2` and `-2` are *associates* (they differ by the unit `-1`). -/
theorem int_dvd_not_antisymm : (2 : ℤ) ∣ -2 ∧ (-2 : ℤ) ∣ 2 ∧ (2 : ℤ) ≠ -2 := by
  refine ⟨⟨-1, by norm_num⟩, ⟨-1, by norm_num⟩, by norm_num⟩

Axioms used: propext, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

Maximal versus greatest, checked by decide on $\{1, \dots, 12\}$ , and Theorem 2 by the counting proof — the down-set of largest size.

maximal_in_one_to_twelveLean 4Proved here from basic factsFormally verified

/-- **The maximal elements of `({1, …, 12}, ∣)` are `7, 8, 9, 10, 11, 12`:** exactly the numbers
`m` with no proper multiple in the set. Checked by `decide`. -/
theorem maximal_in_one_to_twelve :
    (Finset.Icc 1 12).filter (fun m => ∀ x ∈ Finset.Icc 1 12, m ∣ x → x = m) =
      {7, 8, 9, 10, 11, 12} := by
  decide

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

no_greatest_in_one_to_twelveLean 4Proved here from basic factsFormally verified

/-- **…but there is no greatest element:** no `g ∈ {1, …, 12}` is divisible by every member. With
several maximal elements, none of them can be greatest. -/
theorem no_greatest_in_one_to_twelve :
    ¬ ∃ g ∈ Finset.Icc 1 12, ∀ x ∈ Finset.Icc 1 12, x ∣ g := by
  decide

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

exists_maximal_of_finiteLean 4Proved here from basic factsFormally verified

/-- **Every finite non-empty poset has a maximal element.** Choose `m` with the largest number of
elements below it. If `m ≤ x`, everything below `m` is below `x`, so the down-set of `m` is
contained in that of `x`; by the choice of `m` the two down-sets have the same size, hence are
equal. Then `x` (which is below `x`) is below `m`, and antisymmetry gives `x = m`. -/
theorem exists_maximal_of_finite {α : Type*} [PartialOrder α] [Fintype α] [Nonempty α] :
    ∃ m : α, ∀ x, m ≤ x → x = m := by
  classical
  obtain ⟨m, hm⟩ := Finite.exists_max (fun y : α => (Finset.univ.filter (· ≤ y)).card)
  refine ⟨m, fun x hmx => ?_⟩
  have hsub : Finset.univ.filter (· ≤ m) ⊆ Finset.univ.filter (· ≤ x) := by
    intro y hy
    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hy ⊢
    exact le_trans hy hmx
  have heq := Finset.eq_of_subset_of_card_le hsub (hm x)
  have hx : x ∈ Finset.univ.filter (· ≤ m) := by
    rw [heq]
    simp
  simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hx
  exact le_antisymm hx hmx

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

Joins and meets. Unions and intersections are the joins and meets of subsets, the gcd is the meet for divisibility (core Lean's Nat.dvd_gcd_iff), a supremum outside its set, and absorption.

union_isLUBLean 4Proved here from basic factsFormally verified

/-- **In `(P(A), ⊆)` the join of two sets is their union:** `s ∪ t` is an upper bound of
`{s, t}`, and any set containing both `s` and `t` contains `s ∪ t`. -/
theorem union_isLUB {A : Type*} (s t : Set A) : IsLUB {s, t} (s ∪ t) := by
  constructor
  · rintro u (rfl | rfl)
    · exact Set.subset_union_left
    · exact Set.subset_union_right
  · intro u hu
    exact Set.union_subset (hu (Set.mem_insert s {t})) (hu (Set.mem_insert_of_mem s rfl))

Axioms used: No axiomsformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

inter_isGLBLean 4Proved here from basic factsFormally verified

/-- **…and the meet is the intersection**, by the dual argument. So `(P(A), ⊆)` is a lattice. -/
theorem inter_isGLB {A : Type*} (s t : Set A) : IsGLB {s, t} (s ∩ t) := by
  constructor
  · rintro u (rfl | rfl)
    · exact Set.inter_subset_left
    · exact Set.inter_subset_right
  · intro u hu
    exact Set.subset_inter (hu (Set.mem_insert s {t})) (hu (Set.mem_insert_of_mem s rfl))

Axioms used: No axiomsformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

gcd_is_meetLean 4Applies a library theoremFormally verified

/-- **In `(ℕ, ∣)` the meet of `a` and `b` is `gcd(a, b)`:** `d` divides `gcd(a, b)` exactly when it
divides both. This is core Lean's `Nat.dvd_gcd_iff`. (Dually, the join is `lcm(a, b)`.) -/
theorem gcd_is_meet (a b d : ℕ) : d ∣ Nat.gcd a b ↔ d ∣ a ∧ d ∣ b := Nat.dvd_gcd_iff

Axioms used: propext, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

lub_not_memLean 4Applies a library theoremFormally verified

/-- **A least upper bound need not belong to the set:** in `ℚ`, the set of rationals below `1`
has least upper bound `1`, which is not in the set. Mathlib's `isLUB_Iio`. -/
theorem lub_not_mem : IsLUB (Set.Iio (1 : ℚ)) 1 ∧ (1 : ℚ) ∉ Set.Iio 1 :=
  ⟨isLUB_Iio, fun h => lt_irrefl (1 : ℚ) h⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

absorptionLean 4Proved here from basic factsFormally verified

/-- **The absorption law** `a ⊔ (a ⊓ b) = a`, which holds in every lattice: `a` is an upper bound
of `a` and of `a ⊓ b ≤ a`, so the join is at most `a`; and `a ≤ a ⊔ (a ⊓ b)` always. Mathlib's
`sup_inf_self`. Absorption, with associativity and commutativity of `⊔` and `⊓`, characterises
lattices algebraically. -/
theorem absorption {L : Type*} [Lattice L] (a b : L) : a ⊔ (a ⊓ b) = a :=
  le_antisymm (sup_le le_rfl inf_le_left) le_sup_left

Axioms used: No axiomsformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

Well-orders. Theorem 5 by strong induction, exactly as above, and the two non-examples of Proposition 6.

nat_wellOrderedLean 4Proved here from basic factsFormally verified

/-- **ℕ is well-ordered: every non-empty set of naturals has a least element.** Suppose `S` has no
least element. By strong induction no `k` lies in `S`: if `k ∈ S`, then since `k` is not least
there is a smaller `n ∈ S`, contradicting the induction hypothesis for `n`. So `S` is empty. -/
theorem nat_wellOrdered (S : Set ℕ) (hS : S.Nonempty) : ∃ m ∈ S, ∀ n ∈ S, m ≤ n := by
  by_contra h
  have h' : ∀ m ∈ S, ∃ n ∈ S, n < m := by
    intro m hm
    by_contra hne
    exact h ⟨m, hm, fun n hn => not_lt.mp fun hnm => hne ⟨n, hn, hnm⟩⟩
  have key : ∀ k, k ∉ S := by
    intro k
    induction k using Nat.strong_induction_on with
    | _ k ih =>
      intro hk
      obtain ⟨n, hn, hnk⟩ := h' k hk
      exact ih n hnk hn
  obtain ⟨x, hx⟩ := hS
  exact key x hx

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

int_not_wellOrderedLean 4Proved here from basic factsFormally verified

/-- **ℤ is not well-ordered by `≤`:** the whole of `ℤ` (a non-empty set) has no least element,
since `m - 1 < m` for every `m`. -/
theorem int_not_wellOrdered : ¬ ∃ m : ℤ, ∀ x : ℤ, m ≤ x := by
  rintro ⟨m, hm⟩
  have := hm (m - 1)
  omega

Axioms used: propext, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

rat_pos_no_leastLean 4Proved here from basic factsFormally verified

/-- **Nor is ℚ, even on the positive part:** the positive rationals have no least element, since
`0 < m/2 < m` whenever `0 < m`. -/
theorem rat_pos_no_least : ¬ ∃ m : ℚ, 0 < m ∧ ∀ q : ℚ, 0 < q → m ≤ q := by
  rintro ⟨m, hm, hmin⟩
  have := hmin (m / 2) (by linarith)
  linarith

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

Fixed points and Zorn. Knaster–Tarski in four lines, each matching a sentence of the proof; and Zorn's lemma, which Mathlib proves from the axiom of choice (Lean's Classical.choice).

knaster_tarskiLean 4Proved here from basic factsFormally verified

/-- **Knaster–Tarski: every monotone map on a complete lattice has a least fixed point**, namely
`a = inf {x | f x ≤ x}`. For each such `x`, `a ≤ x` gives `f a ≤ f x ≤ x`, so `f a` is a lower
bound and `f a ≤ a`. Then `f (f a) ≤ f a`, so `f a` belongs to the set and `a ≤ f a`. Any fixed
point `b` belongs to the set, so `a ≤ b`. (Mathlib's version is `OrderHom.lfp`.) -/
theorem knaster_tarski {L : Type*} [CompleteLattice L] (f : L → L) (hf : Monotone f) :
    ∃ a, f a = a ∧ ∀ b, f b = b → a ≤ b := by
  set a := sInf {x | f x ≤ x} with ha
  have h1 : f a ≤ a := le_sInf fun x hx => le_trans (hf (sInf_le hx)) hx
  have h2 : a ≤ f a := sInf_le (show f (f a) ≤ f a from hf h1)
  exact ⟨a, le_antisymm h1 h2, fun b hb => sInf_le (show f b ≤ b from hb.le)⟩

Axioms used: No axiomsformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

zornLean 4Applies a library theoremFormally verified

/-- **Zorn's lemma:** in a preorder in which every chain has an upper bound, there is a maximal
element (nothing strictly above it). Mathlib's `zorn_le`, proved there from the axiom of choice;
over ZF the two are equivalent (see the lesson on the axiom of choice). -/
theorem zorn {α : Type*} [Preorder α] (h : ∀ c : Set α, IsChain (· ≤ ·) c → BddAbove c) :
    ∃ m : α, IsMax m :=
  zorn_le h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/OrderTheory.leanTry it in the Lean web editor

Not formalised here: Proposition 1, the linear-extension corollary, the algebraic characterisation of lattices, and the well-ordering theorem (Mathlib: WellOrderingRel), whose proof, like Zorn's lemma, uses choice.

ComputationC

Counting orders, and computing with them

How many partial orders are there on a small set? Every partial order is reflexive, so it suffices to try all choices of the off-diagonal pairs — $2^{12} = 4096$ relations on four elements — and test the axioms. The census shows that total orders and lattices are rare among partial orders, and checks Theorem 2 on every poset with at most four elements. (The number of preorders, $1, 4, 29, 355$ , will reappear in the topologist's viewpoint.)

A census of all partial orders on small setsPythonExhaustive finite checkExact computationComputationally tested

"""How many ways can a small set be ordered? An exhaustive census of posets.

Every partial order on an n-element set is a reflexive relation, so it is
enough to try all 2^(n(n-1)) choices of the off-diagonal pairs. For n <= 4 the
experiment counts the preorders, the partial orders, the total orders and the
lattices among them, and checks on every partial order the lesson's theorem
that a finite non-empty poset has a maximal element - and that "maximal"
and "greatest" really differ. The counts are exact and exhaustive for these
sizes (they agree with the published values: 1, 3, 19, 219 partial orders);
they prove nothing for larger n.
"""

import itertools
import math

def reflexive_relations(n):
    """Yield every reflexive relation on range(n) as a set of pairs."""
    off = [(a, b) for a in range(n) for b in range(n) if a != b]
    diag = {(a, a) for a in range(n)}
    for bits in itertools.product((0, 1), repeat=len(off)):
        yield diag | {p for p, bit in zip(off, bits) if bit}

def is_transitive(rel, n):
    """(a, b) and (b, c) in rel imply (a, c) in rel."""
    return all((a, c) in rel for (a, b) in rel for c in range(n)
               if (b, c) in rel)

def is_antisymmetric(rel):
    """(a, b) and (b, a) in rel imply a = b."""
    return all(a == b or (b, a) not in rel for (a, b) in rel)

def is_total(rel, n):
    """Any two elements are comparable."""
    return all((a, b) in rel or (b, a) in rel
               for a in range(n) for b in range(n))

def maximal_elements(rel, n):
    """Elements with nothing strictly above them."""
    return [m for m in range(n)
            if not any((m, x) in rel and x != m for x in range(n))]

def greatest_element(rel, n):
    """The element above everything, or None."""
    tops = [g for g in range(n) if all((x, g) in rel for x in range(n))]
    return tops[0] if tops else None

def join(rel, n, a, b):
    """The least upper bound of a and b, or None if it does not exist."""
    ups = [u for u in range(n) if (a, u) in rel and (b, u) in rel]
    least = [u for u in ups if all((u, v) in rel for v in ups)]
    return least[0] if least else None

def meet(rel, n, a, b):
    """The greatest lower bound of a and b, or None."""
    return join({(y, x) for (x, y) in rel}, n, a, b)

def is_lattice(rel, n):
    """Every pair has a join and a meet."""
    return all(join(rel, n, a, b) is not None and meet(rel, n, a, b)
               is not None for a in range(n) for b in range(n))

def census(n):
    """Counts for all relations on an n-element set."""
    c = {"preorders": 0, "partial orders": 0, "total orders": 0,
         "lattices": 0, "with greatest": 0, "max ok": True}
    for rel in reflexive_relations(n):
        if not is_transitive(rel, n):
            continue
        c["preorders"] += 1
        if not is_antisymmetric(rel):
            continue
        c["partial orders"] += 1
        c["total orders"] += is_total(rel, n)
        c["lattices"] += is_lattice(rel, n)
        c["with greatest"] += greatest_element(rel, n) is not None
        c["max ok"] = c["max ok"] and bool(maximal_elements(rel, n))
    return c

def main():
    print(" n  preorders  partial  total  n!  lattices  with greatest")
    every = True
    for n in range(1, 5):
        c = census(n)
        every = every and c["max ok"]
        print(f"{n:>2}  {c['preorders']:>9}  {c['partial orders']:>7}"
              f"  {c['total orders']:>5}  {math.factorial(n):>2}"
              f"  {c['lattices']:>8}  {c['with greatest']:>13}")
    print("every partial order (n <= 4) has a maximal element:", every)
    v = {(0, 0), (1, 1), (2, 2), (0, 1), (0, 2)}
    print("the 'V' shape 0 < 1, 0 < 2: maximal", maximal_elements(v, 3),
          "greatest", greatest_element(v, 3), "join(1, 2)", join(v, 3, 1, 2))
    print()
    print("Epistemic status: an exact, exhaustive count for sets of at most")
    print("four elements, agreeing with the known values. It illustrates that")
    print("most partial orders are neither total nor lattices, and confirms")
    print("the maximal-element theorem for these cases only; the lesson proves")
    print("it for every finite poset.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The second experiment computes the Hasse diagram of divisibility on $\{1, \dots, 12\}$ , confirms that the divisors of $60$ form a lattice with $\gcd$ and $\operatorname{lcm}$ as meet and join while $\{1, \dots, 12\}$ does not, and finds the set of vertices reachable in a small graph as a least fixed point — once by iterating from $\varnothing$ , once as the intersection of all pre-fixed points, as in Theorem 7.

Divisibility orders, lattices and a least fixed pointPythonExact computationExhaustive finite checkComputationally tested

"""Divisibility as an order: Hasse diagrams, lattices and a least fixed point.

The experiment lists the covering pairs of ({1, ..., 12}, |) - the edges of
its Hasse diagram - and its minimal and maximal elements; checks that the
divisors of 60 form a lattice with meet gcd and join lcm, while {1, ..., 12}
is not a lattice; and computes a least fixed point two ways, as the
Knaster-Tarski theorem predicts: by iterating a monotone map on the subsets of
a finite set starting from the empty set, and as the intersection of all
sets S with f(S) contained in S. Exact and exhaustive for these examples.
"""

import itertools
import math

def covers(elements, leq):
    """Pairs (a, b) with a < b and nothing strictly between: Hasse edges."""
    return [(a, b) for a in elements for b in elements
            if a != b and leq(a, b)
            and not any(c not in (a, b) and leq(a, c) and leq(c, b)
                        for c in elements)]

def divides(a, b):
    """a | b."""
    return b % a == 0

def maximal(elements, leq):
    """Elements with no strictly larger element."""
    return [m for m in elements
            if not any(x != m and leq(m, x) for x in elements)]

def least_upper_bound(elements, leq, a, b):
    """The join of a and b inside `elements`, or None."""
    ups = [u for u in elements if leq(a, u) and leq(b, u)]
    least = [u for u in ups if all(leq(u, v) for v in ups)]
    return least[0] if least else None

def lattice_check(elements, leq):
    """Return the first pair without a join, or None if all joins exist."""
    for a, b in itertools.combinations(elements, 2):
        if least_upper_bound(elements, leq, a, b) is None:
            return a, b
    return None

EDGES = {0: {1, 2}, 1: {3}, 2: {3}, 3: {4}, 4: set(), 5: {6}, 6: {5}, 7: {0}}

def step(s, start=0, edges=EDGES):
    """f(S) = {start} together with every successor of S: monotone in S."""
    return frozenset({start}) | frozenset(t for v in s for t in edges[v])

def lfp_by_iteration(f):
    """Kleene iteration: empty set, f(empty), f(f(empty)), ... until stable."""
    s, rounds = frozenset(), 0
    while f(s) != s:
        s, rounds = f(s), rounds + 1
    return s, rounds

def lfp_by_prefixed_points(f, universe):
    """Intersection of all S with f(S) a subset of S (Knaster-Tarski)."""
    result = frozenset(universe)
    for r in range(len(universe) + 1):
        for s in itertools.combinations(universe, r):
            s = frozenset(s)
            if f(s) <= s:
                result &= s
    return result

def main():
    nums = list(range(1, 13))
    edges = covers(nums, divides)
    print(f"Hasse diagram of ({{1..12}}, |): {len(edges)} covering pairs")
    print("  " + " ".join(f"{a}-{b}" for a, b in edges[:12]))
    print("  " + " ".join(f"{a}-{b}" for a, b in edges[12:]))
    print("  minimal:", maximal(nums, lambda a, b: divides(b, a)),
          " maximal:", maximal(nums, divides))
    print("  pair with no join in {1..12}:", lattice_check(nums, divides))
    d60 = [d for d in range(1, 61) if 60 % d == 0]
    ok = all(least_upper_bound(d60, divides, a, b) == math.lcm(a, b)
             for a in d60 for b in d60)
    print(f"divisors of 60 ({len(d60)}): every join exists and is the lcm:", ok)
    print("  pair with no join among divisors of 60:",
          lattice_check(d60, divides))
    print()
    fix, rounds = lfp_by_iteration(step)
    meet = lfp_by_prefixed_points(step, range(8))
    print("reachable from 0 in a graph = least fixed point of S -> {0} u succ(S)")
    print(f"  iteration from the empty set: {sorted(fix)} after {rounds} rounds")
    print(f"  meet of all pre-fixed points: {sorted(meet)}")
    print("  the two agree:", fix == meet)
    print()
    print("Epistemic status: exact, exhaustive computations for these finite")
    print("examples. They illustrate the definitions and the Knaster-Tarski")
    print("theorem, which the lesson proves for every complete lattice.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Both are exhaustive and exact for the finite examples computed. They illustrate the theorems; the proofs above cover all posets and all complete lattices.

Exercises

1. Orders, lattices and well-orders

Warm-upHuman

Which of these relations are partial orders (reflexive, antisymmetric, transitive)? (Choose all that apply.)

Choose all that apply

\le

\R

a \mid b

\N

a \mid b

\Z

\subseteq

\mathcal{P}(A)

<

\N

a \preceq b \iff |a| \le |b|

\Z

2. Orders, lattices and well-orders

Warm-upHuman

Consider $\{2, 3, \dots, 10\}$ ordered by divisibility. List all its maximal elements, separated by commas.

3. Orders, lattices and well-orders

Warm-upHuman

In the lattice $(\N, \mid)$ , what is the join (least upper bound) $12 \vee 18$ ?

4. Orders, lattices and well-orders

CoreHuman

How many edges (covering pairs) does the Hasse diagram of $(\mathcal{P}(\{1, 2, 3, 4\}), \subseteq)$ have?

5. Orders, lattices and well-orders

CoreHuman

Theorem 2 says every finite non-empty poset has a maximal element. Which example shows that the word "finite" cannot simply be dropped?

Choose one

(\N, \le)

(\N, \mid)

(\mathcal{P}(\N), \subseteq)

the empty poset

6. Orders, lattices and well-orders

CoreHuman

Which of these totally ordered sets are well-ordered (every non-empty subset has a least element)? (Choose all that apply.)

Choose all that apply

\{1 - \tfrac1n : n = 1, 2, 3, \dots\}

with the usual

\le

\{\tfrac1n : n = 1, 2, 3, \dots\}

with the usual

\le

\{0, -1, -2, \dots\}

with the reversed order

\ge

\{q \in \Q : q \geq 0\}

with the usual

\le

7. Orders, lattices and well-orders

CoreFormal

Which Lean statement says correctly that every finite non-empty poset has a maximal element?

Choose one

theorem t {α : Type*} [PartialOrder α] [Fintype α] [Nonempty α] : ∃ m : α, ∀ x, m ≤ x → x = mtheorem t {α : Type*} [PartialOrder α] [Fintype α] [Nonempty α] : ∃ m : α, ∀ x, x ≤ mtheorem t {α : Type*} [PartialOrder α] [Nonempty α] : ∃ m : α, ∀ x, m ≤ x → x = mtheorem t {α : Type*} [PartialOrder α] [Fintype α] : ∃ m : α, ∀ x, m ≤ x → x = m

8. Orders, lattices and well-orders

StretchHuman

Knaster–Tarski: a monotone map on a complete lattice has a fixed point. Which examples show that one of the two hypotheses cannot be dropped? (Choose all that apply.)

Choose all that apply

x \mapsto x + 1

(\Z, \le)

0 \mapsto 1

1 \mapsto 0

(\{0, 1\}, \le)

x \mapsto x/2

([0, 1], \le)

S \mapsto S

(the identity) on

\mathcal{P}(A)

9. Orders, lattices and well-orders

StretchComputational

Write linear_extension(elements, leq) that lists the elements of a finite poset in an order compatible with leq (a function returning True when $a \le b$ ): whenever $a \le b$ and $a \neq b$ , $a$ must come before $b$ . Use the idea of Corollary 3, or repeatedly take a minimal element.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

Treating "maximal" and "greatest" as synonyms. Greatest means above everything; maximal means nothing is above it. They agree in total orders, but a partial order can have many maximal elements and no greatest one: in $(\{1, \dots, 12\}, \mid)$ there are six maximal elements and no greatest. If a greatest element exists, it is the unique maximal element (Proposition 1) — but a unique maximal element need not be greatest in an infinite poset (take $\N$ together with one extra element $\top$ that is comparable only with itself: $\top$ is the only maximal element, yet it is not above $0$ ).

Misconception

Assuming every partial order is total. Divisibility, inclusion of sets and the product order on pairs all have incomparable elements. Arguments such as "either $a \le b$ or $b \le a$ " are valid only after totality has been established.

Misconception

"The least upper bound of a set belongs to the set." It need not: $\sup\{q \in \Q : q < 1\} = 1$ is not in the set, and in $(\mathcal{P}(A), \subseteq)$ the supremum of $\{\{1\}, \{2\}\}$ is $\{1, 2\}$ . When the supremum does belong to the set, it is the set's greatest element.

Misconception

"A set with a least element is well-ordered." Well-ordering requires that every non-empty subset has a least element. The non-negative rationals have a least element, $0$ , but their subset of positive rationals has none.

Misconception

"Zorn's lemma is proved by climbing until you reach the top." Climbing works for finite posets (Theorem 2). For infinite ones the climb must continue transfinitely, choosing an upper bound at every limit stage — infinitely many arbitrary choices, which is exactly what the axiom of choice provides. Without choice, Zorn's lemma cannot be proved.

ViewpointsH

Many ways of seeing

Topology— Finite topologies are preorders

Every topological space $X$ carries a specialisation preorder: $x \preceq y$ when every open set containing $x$ also contains $y$ (equivalently, $x$ lies in the closure of $\{y\}$ , with the convention that open sets are "up-sets"). For finite spaces the correspondence is perfect: topologies on a finite set are in one-to-one correspondence with preorders on it, the open sets being exactly the up-closed sets, and the space is $T_0$ (points are distinguished by open sets) exactly when the preorder is a partial order. So the census counts topologies too: there are $29$ topologies on a three-point set, the same as the number of preorders. Continuous maps between finite spaces are exactly the monotone maps. In the other direction, every total order generates an order topology, and for a dense total order connectedness is equivalent to completeness — the reason $\R$ is connected and $\Q$ is not (see point-set topology).

Geometry— The Boolean lattice is a cube

The Hasse diagram of $\mathcal{P}(\{1, \dots, n\})$ is the graph of the $n$ -dimensional cube: identify a subset with its indicator vector in $\{0, 1\}^n$ , and two subsets are joined when they differ in one coordinate. Rank (the size of a subset) is height in the cube; the meet and join are coordinatewise minimum and maximum. More generally, the faces of a convex polytope — vertices, edges, faces, …, ordered by inclusion — form a lattice, the face lattice, which captures the polytope's combinatorial shape; the face lattice of a cube, for instance, has $8 + 12 + 6$ elements between the empty face and the whole cube. Product orders on $\R^n$ are geometric too: the elements above a point form a closed orthant, and the Pareto front of a finite set is its set of maximal points.

Combinatorics— Chains, antichains and Dilworth's theorem

In a finite poset, a chain and an antichain share at most one element, so covering the poset by chains needs at least as many chains as the size of the largest antichain. Dilworth's theorem (1950) says this bound is attained: the minimum number of chains covering a finite poset equals the maximum size of an antichain. Its dual, Mirsky's theorem, says the length of the longest chain equals the minimum number of antichains covering the poset. In $\mathcal{P}(\{1, \dots, n\})$ , the largest antichain has $\binom{n}{\lfloor n/2 \rfloor}$ sets — all subsets of the middle size — which is Sperner's theorem (1928). For $(\{1, \dots, 12\}, \mid)$ , the six maximal elements $7, \dots, 12$ form an antichain, and the chains $1 \mid 2 \mid 4 \mid 8$ , $3 \mid 6 \mid 12$ , $9$ , $5 \mid 10$ , $7$ , $11$ cover the poset, so six is the answer to both questions (see combinatorics).

Logic— Implication is an order, and induction is a least fixed point

Propositions ordered by implication ( $p \le q$ when $p$ implies $q$ , up to logical equivalence) form a lattice whose meet is "and" and whose join is "or": a Boolean algebra, the algebraic face of propositional logic (see propositional logic). The Knaster–Tarski theorem is the foundation of inductive definitions: the natural numbers, the well-formed formulas of a logic and the theorems of a proof system are each the least set closed under certain rules — the least fixed point of a monotone operator — and proofs by induction over them are proofs that a property defines a pre-fixed point. In computer science, the meaning of a recursive program is the least fixed point of a monotone map on a lattice of partial functions, and static analysers compute least fixed points by exactly the iteration from the bottom element used in the computation section.

Category theory— A preorder is a category with at most one arrow

A preorder $(P, \le)$ is the same thing as a category with at most one morphism between any two objects: put an arrow $a \to b$ exactly when $a \le b$ ; reflexivity provides identities and transitivity provides composition. Monotone maps are then exactly functors, a supremum is a coproduct, an infimum is a product, a greatest element is a terminal object and a least element an initial object. A pair of monotone maps $f : P \to Q$ , $g : Q \to P$ with $f(p) \le q \iff p \le g(q)$ — a Galois connection — is precisely an adjunction between thin categories, and much of category theory can be first learned in this simplified, ordered setting (see categories and adjunctions).

History & global context

History and global context

Orders of magnitude and of numbers. Comparisons of size are as old as counting, but the idea of a relation that orders only some pairs emerged in the nineteenth century, in the algebra of logic of George Boole, Charles Sanders Peirce and Ernst Schröder, and in Richard Dedekind's work on ideals: Dedekind's "Dualgruppen" (1897, 1900) are what we now call lattices.
Well-orders and choice. Georg Cantor introduced well-ordered sets and ordinal numbers in the 1880s and 1890s. Ernst Zermelo proved in 1904 that every set can be well-ordered, using the axiom of choice he made explicit for the purpose. Felix Hausdorff's Grundzüge der Mengenlehre (1914) developed the theory of ordered sets systematically and stated a maximal principle; Kazimierz Kuratowski (1922) and Max Zorn (1935) gave the forms now used as "Zorn's lemma".
Lattices and fixed points. Garrett Birkhoff's Lattice Theory (1940) established lattices as a field of their own. Bronisław Knaster and Alfred Tarski proved the fixed-point theorem for sets in 1928, and Tarski gave the general lattice version in 1955. Hasse diagrams take their name from Helmut Hasse, who used them in algebraic number theory; Robert Dilworth proved his decomposition theorem in 1950.
Orders at work. Algorithms for ordering tasks consistently with their dependencies — topological sorting — were developed for project planning and computing in the 1950s and 1960s, and today schedule everything from building projects to software compilation.

Which phone is best?

Pictures of orders: Hasse diagrams

Definitions

Examples and non-examples

Maximal elements and suprema

Well-orders

Fixed points and Zorn's lemma

Orders in Lean and Mathlib

Counting orders, and computing with them

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading