CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Erdős-Szekeres monotone subsequence theorem follows by applying Mirsky's theorem to the index-value poset

Statement

Let $r, s \geq 1$ be natural numbers. Every pairwise distinct finite list of reals of length $(r - 1) (s - 1) + 1$ has a strictly increasing sublist of length $r$ or a strictly decreasing sublist of length $s$ .

Facts & Assumptions

Given: Natural numbers $r, s \geq 1$ and a pairwise distinct list $(a_{i})_{i < N}$ of reals with $N = (r - 1) (s - 1) + 1$ .

[F1]

A sublist is selected by strictly increasing indices; it is strictly increasing, respectively decreasing, when its values strictly increase, respectively decrease (A finite list of reals, and its strictly increasing and strictly decreasing sublists).

[F2]

A partial order is reflexive, antisymmetric, and transitive (Partial order and partially ordered set).

[L1]

Mirsky's theorem says that a nonempty finite poset of height $h$ can be covered by $h$ antichains (Mirsky's theorem: the minimum number of antichains covering a finite poset equals its height).

[L2]

If $f : A \to B$ is a function between finite sets and every fibre has at most $q$ elements, then $∣ A ∣ \leq q ∣ B ∣$ (If $∣ A ∣ > k ∣ B ∣$ then every $f : A \to B$ has a fibre with more than $k$ elements, and for nonempty $B$ some fibre has at least $⌈ ∣ A ∣ / ∣ B ∣ ⌉$ elements, by contraposition).

Proof

technique · direct

1.1

If $r = 1$ or $s = 1$ , any one-term sublist has the required kind, so assume $r, s \geq 2$ .

givenF1

1.2

On the index set ${0, \dots, N - 1}$ define $i ⪯ j$ when $i \leq j$ and $a_{i} \leq a_{j}$ . The relation is reflexive and transitive componentwise, while $i ⪯ j ⪯ i$ forces $i = j$ , so it is a partial order. Its chains, read in increasing index order, give strictly increasing sublists because the values are pairwise distinct.

givenF1F2

2.1

Suppose there is no strictly increasing sublist of length $r$ . Then the index-value poset has height at most $r - 1$ , so [L1] covers its indices by at most $r - 1$ antichains. After ordering the covering antichains and removing from each one the indices already assigned to an earlier one, they form a partition into at most $r - 1$ antichains.

step 1.2L1

2.2

In an antichain of the index-value poset, increasing the indices strictly decreases the corresponding values: if $i < j$ then $a_{i} < a_{j}$ would make $i ≺ j$ , while equality is excluded. Hence, if there is no strictly decreasing sublist of length $s$ , every such antichain has at most $s - 1$ members.

step 1.2F1

3.1

Under the simultaneous absence of both required sublists, map each index to the part containing it in the partition from step 2.1. There are at most $r - 1$ parts, and step 2.2 says that every fibre has at most $s - 1$ elements. Thus [L2] gives $N \leq (r - 1) (s - 1)$ , contradicting $N = (r - 1) (s - 1) + 1$ .

step 2.1step 2.2L2

4.1

Therefore at least one of the two sublists exists: a strictly increasing one of length $r$ , or a strictly decreasing one of length $s$ .

step 1.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. Keller and W. T. Trotter, Applied Combinatorics, §6.4 (standard reference, not scraped)