Countability of eventually identity sequences

Stream: Is there code for X?

[Yaël Dillies]

I guess we don't have the fact that functions \N \r \N which are eventually the identity are countable. So how should I go about proving that? Does mathlib know that \N^0 \times \N^1 \times ... is countable?

[Mario Carneiro]

you could use the fact that finsupps are countable in a few ways: build a bijection to nat ->0 nat using elementwise swap 0 n; build an injection to nat ->0 option nat via if x = n then none else some x; or copy and adapt the proof with = n in place of = 0 (and maybe extend to = f n for arbitrary f : nat -> nat)