definition of R

Stream: new members

[Huỳnh Trần Khanh]

i have absolutely no math background btw. how does the definition of real numbers work in mathlib? why "cauchy sequences"?

[Huỳnh Trần Khanh]

i cloned mathlib several days ago and i find mathlib source code really intriguing

[Johan Commelin]

The Cauchy sequence construction is a very common way of constructing real numbers. Another common option is so-called Dedekind cuts.

[Kevin Buzzard]

But the definition doesn't matter, all we need from the real numbers is the basic stuff which mathematicians use, so whatever the definition is, it's the API which counts (eg you can add two real numbers a and b, and a+b=b+a etc)