LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-11

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.

Every finite colouring of $N$ has an infinite colour class, in ZF

Statement

Every colouring of $N$ (The natural numbers $N$ (von Neumann)) by a nonempty finite set of colours has an infinite colour class in the sense of Finite, countably infinite, countable, uncountable. The finite notions are those of The cardinality $∣ A ∣$ of a finite set, and the result is stronger than any fixed finite pigeonhole conclusion from 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.

Facts & Assumptions

Given: A function $c : N \to C$ with $C$ nonempty and finite.

[L1]

A finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition).

[L2]

A subset of $N$ is finite if it is bounded and countably infinite if it is unbounded (Every subset of an at most countable set is at most countable).

Proof

technique · contradiction

1.1

Suppose every fibre $c^{- 1} ({i})$ , for $i \in C$ , is finite. These fibres are pairwise disjoint and their union is $N$ .

assume-contra

2.1

Iterating [L1] over the finite set $C$ makes their union finite. This contradicts the infinitude of $N$ , so at least one fibre is not finite. That fibre is a subset of $N$ , and [L2] therefore makes it countably infinite.

step 1.1L1L2discharge-contradiction∎

Depends on

Used by

Infinite Ramsey theorem on ℕ: every finite colouring of [ℕ]ᵏ has an infinite monochromatic set, in ZF Theorem

Dependency tree · two levels

38 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

I. B. Leader, Ramsey Theory, proof of Theorem 1 (standard reference, not scraped)

Every finite colouring of NN has an infinite colour class, in ZF