I've posted about this a few times but let me try to do so more clearly. How do we, in #constructiveMathematics , show that a set is countably infinite (that is, there is a bijection between our set and the set of natural numbers)? There's a theorem for this which is elegant and also handles some of the trickier cases such as showing that the set of rational numbers is countably infinite. 1/5
Theorem: a set is countably infinite if and only if it has decidable equality, is infinite, and is countable.
Decidable equality: for any two elements of the set you can say they are equal or they are not equal. (examples: integers, rational numbers, the set { 3, π })
Infinite: there is a one-to-one mapping from the natural numbers into the set (examples: real numbers, the set of functions from integers to integers)
Countable: there is a surjection from the natural numbers to the set. 2/5
To apply this to the rational numbers:
* decidable equality on the integers from induction, and on the rationals because p/q = m/n iff pn = qm
* infinite because the natural numbers are a subset of the rationals
* countable because you can enumerate numerators and denominators (note that this isn't a bijection because you have counted one half many times - as 1/2, 2/4, 3/6 and so on) 3/5
One technical detail: usually countable is defined by a surjection onto the disjoint union of a set and a fixed set with one element. However, that is equivalent to the simpler definition above if the set is known to have an element, and every infinite set has an element. 4/5
Metamath references:
* https://us.metamath.org/ileuni/ctinf.html - A set is countably infinite if and only if it has decidable equality, is countable, and is infinite
* https://us.metamath.org/ileuni/qnnen.html - The rational numbers are countably infinite
* https://us.metamath.org/ileuni/ctm.html - Two equivalent definitions of countable for an inhabited set
5/5