>>12438872just a gist:
we can define a real number as an indexed pair, first being a whole number, the second being an infinite sequence of whole numbers from [0,9], such that what you know and love as (pi) is understood as (3, [1,4,1,5,....])
as long as you define it such that 0.999... = 1.000 and so on for other cases (only trailing 9s colliding with a XX000... are an issue), and that addition and stuff are of common sense behavior, you can show that this system is isomorphic to:
the minimal extension of Q that satisfies completeness (the only total ordered field, up to isomorphism)
dedekind cuts (define each real number as a pair of rationals: the ones larger than "it", and the ones smaller than "it")
(i think?) smallest space where cauchy sequences converge
