# Are there rigorous formulation and proof of the pigeonhole principle?

The well known and intuitive pigeonhole principle states that if $n$ items are put in $m$ containers, and $n>m$, then there is at least one container which has more than one object.

I've always relied on this principle when solving combinatorics problems for the mathematical olympiads, where a high level of formalization is not necessary, but recently I've seen it in a group theory proof, so I wonder: is there a mathematically formal and rigorous formulation of this principle and, if so, what is its proof?

• The problem is that you need to first define what it means by "$n$ distinct items", otherwise everything you do will ultimately be based on intuition of what really this means, including the 'obviously true' proof by angryavian. Dec 28, 2014 at 16:28
• Just for example, from the Wikipedia article would you accept "there does not exist an injective function on finite sets whose codomain is smaller than its domain" as a formal and rigorous formulation of the principle? If so then then of course the proof depends on precisely how you formalise functions and natural numbers, and is mostly boring details, and the various answers below omit those boring details in different ways. But is this even the principle itself, or just the principle applied to sets and functions and such, not actual "items" and actual "boxes"? Dec 28, 2014 at 18:59
• To be clear, just accepting the pigeonhole principle as an obvious fact is rigorous, because it's so patently obvious. You want a formal proof, but formality and rigor are distinct notions. Dec 29, 2014 at 0:33
• @JackM I am not sure I fully agree with the distinction between formality and rigor in response to the OP's question. To me, induction is almost as patently obvious as the pigeonhole principle, but then I am reminded of the foundational problems of dismissing such processes as such. The genuine difficulty that people have answering the question is not a testament to the OP's insistence on formality, but on rigor. After all, no circular argument is rigorous and this is a genuine pitfall as far as proving the pigeonhole principle is concerned. Dec 29, 2014 at 8:23
• A further problem there is that some obvious things either aren't true (in which case asserting them is really bad news), or else asserting their negation is both interesting and consistent with existing axioms (in which case asserting the obvious thing might be missing out on something valuable). Taking an axiom of course is both rigorous and formal, but you still have to be able to state it unambiguously. How to do that is the first part of the question, even if you feel it can't or shouldn't be proved, and therefore skip the second part :-) Dec 30, 2014 at 18:54

Yes and no. A fairly precise statement of the pigeonhole principle would be:

If $A$ and $B$ are sets, and $A$ has more elements than $B$, and $f$ is a function $A\to B$, then $f$ is not injective.

Can it be proved? That depends. In particular, what does "$A$ has more elements than $B$" mean? In the usual development of set theory we use this phrase to mean the same as "$A$ has larger cardinality than $B$", which again means

There is an injective function $B\to A$, but there is no injective function $A\to B$.

So if we use that as our definition, the pigeonhole principle is not a matter of proof -- instead it is part of the definition of what it means for one set to be larger than the other.

Of course, once we define natural numbers, we might want to prove a "finite pigeonhole principle":

If $m$ and $n$ are naturals, and $m>n$, and $A$ has $m$ elements and $B$ has $n$ elements, and $f$ is a function $A\to B$, then $f$ is not injective.

Then all we have to do is to prove this from a definitions of "has $m$ elements" and "$m<n$".

The first of these is fairly easily done, because in the usual development, the natural number $m$ is represented by the set $\{0,1,2,\ldots,m-1\}$ and "has $m$ elements" means to be in bijective correspondence by precisely that set. So when we strip away those bijections, what we have to prove is that if $m>n$ and $f:m\to n$, then $f$ is not injective.

This would be trivial (and pointless) if we're using the cardinality definition of what $m>n$ means -- so even though that is the most common choice, let's assume that we want to define $m>n$ to mean "there is a natural $a$ such that $n+a+1=m$.

The actual content of the proof now is to show that these two competing definitions of $>$ agree! Of course we first need to define addition, but once we have done that, it is a fairly simple matter of induction.

First we prove that $|m+1|>|m|$ (as cardinals) for all $m$. The base case $m=0$ is easy. $0$ is the empty set, so there is no function for $1\to 0$ at all, so in the impossible case that we get one, we can safely claim it will be non-injective.

For the induction case, assume that $|m+1|>|m|$ and we need to show that $|m+1+1|>|m+1|$. Let $f: (m+1+1)\to(m+1)$ be given, and let $b=f(m+1)$

$$g:(m+1)\to m : x \mapsto\begin{cases}f(x) & \text{when }f(x)\ne m \\ b & \text{when }f(x)=m \end{cases}$$

Then by the induction hypothesis $g$ is not injective, so there is $p$ and $q$ with $g(p)=g(q)$. If $f(p)=f(q)$ then $f$ is not injective, and we're done. Otherwise $f(p)\ne f(q)$, but this can only be the case if one of them is $m$ and the other is $b$. But then either $f(p)$ or $f(q)$ equals $f(m+1)$, and $f$ is again not injective.

Now to complete the proof, we just have to handle the case where $a\ne 0$ in $|m+a+1|>|m+1|$. By this time we hopefully know that addition is commutative and associative, so $m+a+1=m+1+a$. And so if we have $f:(m+a+1)\to (m+1)$, then it is also $((m+1)+a)\to(m+1)$, and its restriction to $(m+1)$ is not injective. A restriction of an injective function would itself be injective, so $f$ is not injective. (Whew!).

(... except that we also ought to prove along the way that $p+a\subseteq p$ with the standard representation of the natural numbers; otherwise restricting the last $f$ to $(m+a)$ doesn't make sense).

For a third option, we could also have said that $m>n$ means that $n\in m$ for the set representation of the numbers. That would need a different proof from the induction above.

But all in all, these proofs are not very enlightening about the pigeonhole principle. Intuitively I would say that the pigeonhole principle is itself at least as obvious as it is that $n+a+1=m$ is a good definition of $m>n$. So what the proof actually proves could be argued to be just that the $n+a+1$ definition is reasonable. And this would also be the case for the $n\in m$ alternative.

• +1 for noting that, at least for infinite sets, the pigeonhole principle is true by definition. Dec 29, 2014 at 15:43
• is there a way to do this without cardinals? Sep 21, 2020 at 16:16

Let $X$ be a (finite) set of order $n$, and let $S_1, \dots, S_m\subset X$ with $\bigcup S_i = X$. The pigeonhole principle then asserts that if $m < n$, then some $\#S_i > 1$. For if all $\#S_i \leq 1$, then $n = \#X \leq \#S_1 + \cdots + \#S_m \leq m$.

• This would be more elegant as a direct proof. You prove the bound that if all the $S_i$ have no more than one element, then $$\#X \leq \#S_1+\ldots+\#S_m \leq m$$ which can be written as $n\leq m$. And we can take the contrapositive of that and thereby reach the hypothesis that $n>m$ at the end of the proof rather than mysteriously assuming it for contradiction before we've proven the bound. Dec 28, 2014 at 22:11
• @Meelo: Good point. I've changed the post. Dec 28, 2014 at 22:56
• The first inequality on your last line is totally not obvious and is equivalent to the pigeonhole principle! Dec 29, 2014 at 0:53
• It's a bit difficult to provide a rigorous proof of something as simple as the pigeonhole principle without knowing first what's taken as given or known or axiomatic. The argument I gave above boils down to showing that $\#(A\cup B) \leq \#A + \#B$, and there are quite a few ways of doing so. Since we're only dealing with finite sets, it's simple enough to proceed by induction, say invoking the construction of $\mathbb{N}$ in ZF. If[...] Dec 29, 2014 at 2:01
• ...you want to explicitly show that the sets $\{0, \dots, n\}$ and $\{0, \dots, m\}$ don't have the same cardinality for $n\not = m$, that's straightforward enough to do, but not something I'd normally bother to do unless the original question specific mentions that setting. Maybe the better solution is just to talk about some basic set theory and notation of cardinality; it could be overkill for a question that's only dealing with finite positive integers, though. Dec 29, 2014 at 2:04

A proof by induction on $m$ is quite flexible in terms of how it's formalised, that is to say "basically the same proof" will work in different systems. Outline:

Base case $m = 1$, if more than one item is put in exactly one box, then that box contains all the items. So at least one box has more than one item.

Suppose for the inductive step that whenever more than $k$ items are placed in exactly $k$ boxes then at least one box contains more than one item.

Now, place more than $k+1$ items in exactly $k+1$ boxes. Consider two cases of what is in the first box:

• More than one item. Then one of the boxes (namely the first) contains more than one item.
• 1 or 0 items. Then the remaining items (of which there are more than $k + 1 - 1 = k$) were placed in the other boxes (of which there are exactly $k$) and therefore by the inductive hypothesis one of the boxes contains more than one item.

So either way, at least one box contains more than one item and the induction is complete.

Note: if feeling brave, take the base case as $m = 0$, and state/show that it is not possible to put more than $0$ items into $0$ boxes at all. Proofs by induction where the base case is vacuously true are more fun ;-)

Now, how to rigorously formalise this proof depends firstly on how you formalise "putting items in boxes", and secondly on how you formalise the natural numbers. You could do the latter either by axiomatizing a Peano system or using the common set-theoretical construction. You could do the former either by defining a partition of a set with $n$ elements, where there are $m$ sets in the partition, so $x \in y$ means "item $x$ is in box $y$". Or (equivalently) by a function from a set of size $n$ to a set of size $m$, where $f(x) = y$ means "item $x$ is in box $y$". Or some other way. But in order to talk about the size of a set, we need a formalisation of "size" too. Developing that and showing the necessary properties is potentially the first two or more lectures of a "foundations of mathematics" course, and if anyone can fit it in a reasonably-sized answer to this question then I tip my hat to them! I'm reminded of Russell and Whitehead's Principia Mathematica, where page 379 contains proposition 54.43, together with the remark "From this proposition it will follow, when arithmetical addition has been defined, that $1 + 1 = 2$". A fully formal statement and proof of even the simplest thing can be a major undertaking, it's all a matter of where you start.

I reckon you can fill out the details in my proof by induction in any formalism you're inclined to choose, because all I need is the principle of induction, the ability to consider the first box, the ability to consider "the remaining items" after discounting 0 or 1 of them, and a lemma I snuck past without stating, that if you have $n$ items and set one aside then there are $n-1$ others. That can be proved by induction and used, together with some arithmetic, to prove the two claims in the inductive step about the numbers of the remaining items and remaining boxes.

There's probably some really good way to formalise these features (plus anything else I used without noticing), and then show that any logical system that has those things proves its own version of the Pigeonhole Principle, but I don't have the theory to do that myself. Similarly, each of the other answers here uses certain properties of the system it works in, and wherever those properties can be assumed or proved, that proof of the Principle works.

To add to the proofs offered here, I recently drafted a computer verified proof of the Pigeonhole Principle in Coq. I proceed using a proof by contradiction.

I first prove that, if each container is either empty or contains a single item, the number of items in all of the containers must be less than the number of containers (num_things_num_containers). Then I show that if, the total number of items in all of the containers is more than the number of containers then the assumption that all of the containers were either empty or contained a single item is false (lemma_0). I then show that this is equivalent to saying that there exists a container that is not empty or contains a single value (lemma_1). Finally I conclude by showing that this statement is equivalent to saying that there exists an element that contains more than one item, which proves the pigeonhole principle.

The full development can be found here: https://github.com/llee454/pigeons/blob/master/pigeons.v .

(**
This module presents a proof of the pigeon hole principle, which
states that if you place n things into m containers, and n >
m, then one or more of the containers have more than one thing
in it.
Our proof proceeds by contradiction. We first show that
if we have a collection of containers, cs, where every container
is either empty or has a single item in it, then the number of
items contained in all of the containers is less than or equal
to the number of containers.
Then we show that if, the number of items contained within a
collection of containers is greater than the number of containers,
and every container is either empty or has a single item in it,
we have a contradiction. Accordingly, we cannot place n items
into m collections without placing more than one item in a single
container.
Copyright (C) 2018 Larry D. Lee Jr. <llee454@gmail.com>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this program. If not, see
*)

Require Import base.
Require Import List.
Require Import Lt.          (* for le_not_lt *)
Require Import Compare_dec. (* for le_dec *)
Require Import PeanoNat.    (* for Nat.nle_succ_0 *)

(** * I. Basic Concepts *)

(** Represents things (such as pigeons). *)
Parameter thing : Set.

(** Represents containers (such as cubbies). *)
Definition container := list thing.

(** Represents some collection of containers. *)
Definition containers := list container.

(** Counts the number of things in a container. *)
Definition container_num_things := length (A := thing).

(** Counts the number of containers. *)
Definition num_containers := length (A := container).

(** Counts the number of things in some containers. *)
Definition num_things (cs : containers) : nat
:= fold_right (fun c n => container_num_things c + n) 0 cs.

(**
Accepts a container and asserts that it is either
empty or has only one item in it.
*)
Definition container_ok (c : container) : Prop
:= container_num_things c <= 1.

(**
This lemma proves that the OK predicate is
decideable.
Note: we will need this when proving that
[~ Forall container_ok] implies
[Exists ~ container_ok].
*)
Definition container_ok_dec
:  forall (c : container), {container_ok c}+{~ container_ok c}
:= fun c => le_dec (container_num_things c) 1.

(**
Accepts a set of containers and asserts that
all of the containers are either empty or only
contain a single item.
*)
Definition containers_ok (cs : containers) : Prop
:= Forall container_ok cs.

(** * II. Auxiliary Theorems *)

(**
Accepts a predicate, [P], and a list, [x0 ::
xs], and proves that if [P] is true for every
element in [x0 :: xs], then [P] is true for
every element in [xs].
*)
Definition Forall_tail
:  forall (A : Type) (P : A -> Prop) (x0 : A) (xs : list A), Forall P (x0 :: xs) -> Forall P xs
:= fun _ P x0 xs H
=> let H0
:  forall x, In x (x0 :: xs) -> P x
:= proj1 (Forall_forall P (x0 :: xs)) H in
let H1
:  forall x, In x xs -> P x
:= fun x H2
=> H0 x (or_intror (x0 = x) H2) in
proj2 (Forall_forall P xs) H1.

Arguments Forall_tail {A} {P} x0 xs.

(**
Accepts two predicates, [P] and [Q], and a
list, [xs], and proves that, if [P -> Q],
and there exists an element in [xs] for which
[P] is true, then there exists an element in
[xs] for which [Q] is true.
*)
Definition Exists_impl
:  forall (A : Type) (P Q : A -> Prop),
(forall x : A, P x -> Q x) ->
forall xs : list A,
Exists P xs ->
Exists Q xs
:= fun _ P Q H xs H0
=> let H1
:  exists x, In x xs /\ P x
:= proj1 (Exists_exists P xs) H0 in
let H2
:  exists x, In x xs /\ Q x
:= ex_ind
(fun x H2
=> ex_intro
(fun x => In x xs /\ Q x)
x
(conj
(proj1 H2)
(H x (proj2 H2))))
H1 in
(proj2 (Exists_exists Q xs)) H2.

Arguments Exists_impl {A} {P} {Q} H xs H0.

(** * III. Fundamental Proof *)

(**
This theorem proves that given a collection
of containers, where every container is either
empty or has one item in it, then the number
of items contained in all of the containers
must be less than or equal to the number
of containers.
*)
Definition num_things_num_containers
:  forall cs : containers,
containers_ok cs ->
num_things cs <= num_containers cs
:= let T cs := containers_ok cs -> num_things cs <= num_containers cs in
list_ind T
(* I. case where there are no containers. *)
(fun _ => le_0_n 0)
(* II. case where there is more than one container. *)
(list_ind
(fun xs => forall cs, T cs -> T (xs :: cs))
(* II.A. case where the first container is empty. *)
(fun cs
(H  : T cs)
(H0 : containers_ok (nil :: cs))
=> let H1
:  num_things cs <= num_containers cs
:= H (Forall_tail nil cs H0) in
(le_S
(0 + num_things cs)
(num_containers cs)
(H1 || a <= num_containers cs @a by plus_O_n (num_things cs))))
(* II.B. case where the first container has one or more things in it. *)
(fun x0
=> list_ind
(fun xs => _ -> forall cs, T cs -> T ((x0 :: xs) :: cs))
(* II.B.1. case where the first container has only one thing in it. *)
(fun _ cs
(H  : T cs)
(H0 : containers_ok ((x0 :: nil) :: cs))
=> let H1
:  num_things cs <= num_containers cs
:= H (Forall_tail (x0 :: nil) cs H0) in
le_n_S (num_things cs) (num_containers cs) H1
|| a <= S (num_containers cs) @a by Nat.add_1_l (num_things cs))
(* II.B.2. case where the first container has two or more things in it. *)
(fun x1 xs _ _ cs
(H  : T cs)
(H0 : containers_ok ((x0 :: x1 :: xs) :: cs))
=> False_ind
(num_things ((x0 :: x1 :: xs) :: cs) <= num_containers ((x0 :: x1 :: xs) :: cs))
((Nat.nle_succ_0 (length xs))
(le_S_n (S (length xs)) 0 ((Forall_inv H0) : S (S (length xs)) <= 1)))))).

(** * IV. The Pigeonhole Principle *)

(**
This lemma proves that if we have a collection
of containers and the number of things in the
containers is greater than the number of the
containers then not all of the containers can
be empty or have only one thing in it.
*)
Definition lemma_0
: forall cs : containers,
num_things cs > num_containers cs ->
~ containers_ok cs
:= fun cs
(H  : num_containers cs < num_things cs)
(H0 : containers_ok cs)
=> le_not_lt
(num_things cs)
(num_containers cs)
(num_things_num_containers cs H0)
H.

(**
This lemma proves that if we have a collection
of containers and the number of things in the
containers is greater than the number of
containers, then one of the containers cannot
be empty or have only one item in it.
*)
Definition lemma_1
:  forall cs : containers,
num_things cs > num_containers cs ->
Exists (fun c : container => ~ container_ok c) cs
:= fun cs H
=> neg_Forall_Exists_neg container_ok_dec (lemma_0 cs H).

(**
This theorem proves that if we are given a
collection of containers and the number of
things in those containers is greater than the
number of containers, then one or more of the
containers has more than one thing in it.
*)
Definition pigeonhole_principle
:  forall cs : containers,
num_things cs > num_containers cs ->
Exists (fun c : container => container_num_things c > 1) cs
:= fun cs H
=> Exists_impl
(fun c (H0 : ~ container_ok c)
=> not_le (container_num_things c) 1 H0)
cs
(lemma_1 cs H).

• Reviewers: the link target is not really source code, but is a formalized proof. Aug 23, 2018 at 0:30
• Welcome on the MathSE! It seems to be a very useful answer. However, the site has a rule that anything what you link here, should have also - at least a short - excerpt what is there. It is because to avoid link rot (your posts should be comprehensible years later, too). I suggest to create a short manual excerpt where you explain how your proof works. Aug 23, 2018 at 0:33
• Hi, thanks for the explanation, I'll inline the code along and include a highlevel explanation. Aug 24, 2018 at 15:11

Theorem: Let $n_i$, $1\leq i \leq n$ be a collection of natural numbers such that $\sum_i n_i >n$. Then $\exists i: n_i > 1$.

Proof: assume that $\forall i: n_i\leq 1$. Then $\sum_i n_i \leq n\cdot 1 < \sum_i n_i$, contradiction. $\square$

I don't claim this is the ultimate proof for the pigeon hole principe; what you consider the ultimate proof depends on what axioms you feel most comfortable with. In particular, if someone thinks the pigeon hole principle is sufficiently basic to use as an axiom, then I'm fine with that. It is, however, the way I internally justify the principle whenever feel uncomfortable using it, based on principles that I do feel comfortable with.

Exercise: Let $n_i$, $1\leq i \leq n$ be a collection of natural numbers such that $\sum_i n_i >m$. Then $\exists i: n_i > m/n$.

For any class $S$ and natural number $n$, define $\#(S) = n$ to mean that $n$ is the minimum natural number such that there is a injection $f$ from $S$ into $\mathbb{N}_{< n}$. Note that if there is an injection from $S$ into $\mathbb{N}_{<k}$ for some $k \in \mathbb{N}$, the existence of the minimum such $k$ follows from the well-ordering which is equivalent to induction. If we say that $S$ is finite if such an injection exists, then we have pigeonhole for any finite sets $S$ and $T$ such that $\#(S) > \#(T)$, simply by definition as follows. If there is an injection $f$ from $S$ to $T$, let $g$ be an injection from $T$ into $\mathbb{N}_{< \#(T)}$, and then $g \circ f$ is an injection from $S$ into $\mathbb{N}_{< \#(T)}$, which implies that $\#(T) \le \#(S)$, which is a contradiction.

Note that the above is a proof only for the finite case, but uses only Peano arithmetic, and is most in line with intuition. The intuition is that if you have $n$ distinct objects, you need at least $n$ natural numbers to label them all such that each has a different label, hence any injection (different labels for different objects) cannot use only natural numbers from $0$ to strictly less than $n-1$. And we want to use the least possible labels, which we can by the well-ordering principle. This application of the well-ordering principle can itself be proven from induction intuitively. It starts by asking, can we use only labels less than $0$? If so, $0$ is the minimum possible. If not, can we use only labels less than $1$? If so, $1$ is the minimum possible. If not, can we use only labels less than $2$? ... If there is no minimum, there will not be any labeling that uses bounded labels, which intuitively happens when we have infinitely many distinct objects, and so we use this labeling criterion to define finiteness.

A nice way to state this which doesn't rely on counting (and works with cardinality rather than just the finite size of a set) would be to phrase it as follows:

Let $P$ be a set and $S$ be a partition of $P$ with $|S|<|P|$. There is some $s\in S$ with at least two elements.

which, intuitively says that, in the finite case, if $P$ has $n$ elements, then any partition of it into $n-1$ or fewer sets will have one element of the partition with multiple members. The proof of this is easy. If we define $f:P\rightarrow S$ to be the function such that $p\in f(p)$ - that is, $f(p)$ is the element of the partition containing $p$ - then, it follows that the preimage $f^{-1}[S]=S$. If every $S$ had at most one element, this would be equivalent to saying that $f$ is injective and therefore that $|S|\geq|P|$. Since, on the contrary, $|S|<|P|$ it must be that $f$ is not injective and therefore that some $S$ has more than one element.

This suffices to show a statement like, "You cannot partition $\mathbb R$ into countably many bins without one bin having multiple elements" at the same time as "If you have a set of $n$ pigeons, you cannot partition them into $n-1$ holes without having one hole with at least $2$ pigeons"

Notice that this proof does require knowing that the cardinality of $A=\{1,2,\ldots,i\}$ is greater than that of $B=\{1,2,\ldots,j\}$ for $i>j$. We can prove this by induction on $j$. It clearly holds for $j=0$, since there is no function to the empty set from a non-empty set. For the inductive step, notice that if $f:A\rightarrow B$ is an injection, then $$g(a)=\begin{cases}f(a) &&\text{if }f(a)<f(i)\\f(a)-1 &&\text{if }f(a)>f(i)\end{cases}$$ is an injection $\{1,2,\ldots,i-1\}\rightarrow\{1,2,\ldots,j-1\}$, which cannot exist by inductive hypothesis.

• This doesn't answer the question because it is essentially saying that if we define $S$ to be smaller in size than $T$, there is no injection from $T$ into $S$, and then there is nothing to prove! Dec 29, 2014 at 0:49
• @user21820 I've been thinking about that very issue since I posted it; I added an inductive proof of the fact. I feel like there ought to be a more elegant proof of "finite ordinals are cardinals" than this one though. Dec 29, 2014 at 1:31
• Yes that is why I did not use a bijection to the "first k naturals" in my answer. Also, I didn't think "..." is very satisfying for something that is supposed to be rigorous so I chose to go with "injection $f$ from $S$ into $\mathbb{N}_{< k}$" which can be expressed without even talking about the set of natural numbers via "injective natural-valued function $f$ on $S$ such that $f(x) < k$ for any $x \in S$". Dec 29, 2014 at 1:37
• @user21820 I would argue that bijection with first $k$ naturals is the best way to do this - we count, by bijections, not injections. I like your answer, but it does not prove that finite ordinals are cardinals - i.e. that there exists a set with $\#(S)=n$ for all $n$. Using the naturals is justified since all well-orders on finitely many elements are isomorphic - and the fundamental idea here is that, using ordinal arithmetic, if there is an injection $1+A$ to $1+B$, there too is $A$ to $B$ - and thus there can be none from $C+A$ to $C$ if $C=1+1+\ldots+1$, as there would be one $A$ to $0$. Dec 29, 2014 at 1:46
• Hmm I don't see that much difference between using bijections and using injections. The image under an injection is in bijection with the original after all. In fact it is easy for me to prove the bijection using my definition, because we can't have any unused naturals less than $k$ otherwise there is a better labeling. Dec 29, 2014 at 1:53

If $f:X\rightarrow Y$ is a map, with $X$ and $Y$ finite sets and $\mathrm{card} \ X> \mathrm{card} \ Y$ then $f$ cannot be injective. (The proof is obivous. Upon request: if $f$ were injective, then $\mathrm{card} \ X=\mathrm{card} \ f(X) \leqslant \mathrm{card} \ Y$ which is a contradiction.)

• The proof is "as obvious" as the pigeonhole principle: do you have it? Produce it, otherwise you don't have it. Dec 28, 2014 at 16:22
• @Timbuc: of course I have it. Dec 28, 2014 at 16:48
• More work needs to be done otherwise it is not at all obvious how "finiteness" is used. Dec 28, 2014 at 16:50
• @user21820: finiteness is redundant. Dec 28, 2014 at 16:51
• Yes but I mean that all the details are hiding in $\text{card}$... Dec 28, 2014 at 16:53