The colouring is a plain function on $Sym2 (Fin n)$, mathlib's type of unordered pairs; no notion of colouring is introduced. Colourings assign a colour to the degenerate pairs $s(u, u)$ as well, and the conclusion ignores them — $Set.Pairwise$ constrains distinct elements only — so colourings of the edges of the complete graph are exactly the functions considered here, restricted along an inclusion that changes nothing.

Sizes are stated as "at least": a monochromatic set of size at least s contains one of size exactly s, and the stated form is what every application uses. All statements of this submission range over the canonical carriers $Fin n$ and over all $n$ beyond the bound, so the theorem applies to a set of any size by transport along a bijection.

The Ramsey number itself is deliberately not defined. The archive's convention for a numeric parameter would be $sInf {N | …}$, but no statement of this submission consumes a numeric bound, so such a definition would be endorsement surface that nothing uses; the existential carries the whole content.

No hypothesis is placed on the number of colours: for $k = 0$ there is no colouring of the pairs of a nonempty set at all, so the statement holds vacuously with $N = 1$.