I found this exercise in a publication from leanprover. The publication was about equinumerosity (two sets might be called equinumerous if they have the same cardinality). I hope someone can point me in the right direction.

Exercise

If f and g are functions from N to N, we say "g eventually dominates f" if there is some n such that, for every $\displaystyle m \ge n$, we have $\displaystyle g\left( m \right) > f\left( m \right)$. Informally we say "from some point on, g is always greater than f."

Let $\displaystyle {f_0},\,{f_1},\,{f_2},\, \ldots $ be a sequence of functions from N to N indexed by the natural numbers. Show that there exists a function g that eventually dominates each f.

My thoughts

If I'm allowed to use a different function g for each f, then this seems very simple. I could write $\displaystyle {g_i}\left( n \right) = {f_i}(n) + i - n + 2$. I put in the 2 so that there would always be some values for which g does not dominate f, even when i is small.

Is that what I'm supposed to do? I'm not sure where this exercise is supposed to lead me.

I suspect they want a single function $\displaystyle {g}$ that will dominate every $\displaystyle {f_i}$. How do I do that? I'm familiar with the Cantor Pairing Function. I'm sure that a bijection exists between $\displaystyle \left\langle {i,j} \right\rangle \in N \times N$ and $\displaystyle {f_i}(n)$. But then the sequence isn't right. The n that would get me to $\displaystyle {f_i}(n)$ isn't the same n as you see in the $\displaystyle {f_i}$ function. If I increment n, I'll wind up with something like $\displaystyle {f_{i+1}}(n-1)$, moving up a diagonal.

Any ideas?