Generally the pigeonhole principle is formulated as follows
If there are $m$ pigeons and $n$ holes, such that $m>n$, then there must exist at least one hole that shares more than $1$ pigeon
However this seems to just be a fairly direct consequence of injective functions. i.e.
Let $P$ be the set of pigeons and $H$ the set of holes, with $|P|>|H|$. $\forall f:P\rightarrow H$, $f$ is not injective
Is this an ok way to think about the pigeonhole principle, or is there more to it that I am missing?