CorollaryStatement: AI-generatedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

Infinite Ramsey holds for every set equipped with an injection from $\mathbb N$

Statement

Let $X$ be a set equipped with an injection $j:\mathbb N\to X$ . For every positive $k$ , every finite colouring of $[X]^k$ has an infinite monochromatic subset contained in $j[\mathbb N]$ . The terms injection, equinumerous and monochromatic are those of Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A \preceq B$ and Finite colourings of $k$ -element subsets, monochromatic sets, and the arrow notations $N\to(s,t)^2$ and $N\to(r)^k_c$ .

Facts & Assumptions

Given: An injection $j:\mathbb N\to X$ and a finite colouring $c:[X]^k\to C$ .

[L1]

Every finite colouring of $[\mathbb N]^k$ has an infinite monochromatic set, in ZF (Infinite Ramsey theorem on $\mathbb N$ : every finite colouring of $[\mathbb N]^k$ has an infinite monochromatic set, in ZF).

[F1]

$f$ is injective (one-to-one) if $f(x) = f(y)$ implies $x = y$ (Injection, surjection, bijection).

Proof

technique · direct

1.1

Define a colouring of $[\mathbb N]^k$ by $A\mapsto c(j[A])$ . Injectivity in [F1] makes $j[A]$ a $k$ -element set, so [L1] gives an infinite homogeneous $H\subseteq\mathbb N$ .

L1F1

2.1

By [F1], the restriction $j|_H$ is a bijection from $H$ to $j[H]$ , so $j[H]$ is infinite. The pullback definition shows every $k$ -subset of $j[H]$ has the same $c$ -colour.

step 1.1F1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 35 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Infinite Ramsey holds for every set equipped with an injection from N\mathbb NN