Maybe worth checking out if you want a formal (as in machine checkable) definition of reals:

https://leanprover-community.github.io/mathlib-overview.html