michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/data/real): update md

Browse source
This commit is contained in:
Rob Lewis 2015-06-09 15:43:43 +10:00
parent e112468f99
commit b1aea149db
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/data/real/real.md
View file

@ -1,8 +1,9 @@
data.real data.real
======== ========
The real numbers. The real numbers: classically, as a quotient type; constructively, as a setoid.
* [basic](basic.lean) : the reals as a commutative ring (constructive) * [basic](basic.lean) : the reals as a commutative ring (constructive)
* [order](order.lean) : the reals as an ordered ring (constructive) * [order](order.lean) : the reals as an ordered ring (constructive)
* [division](division.lean) : the reals as a discrete linear ordered field (classical) * [division](division.lean) : the reals as a discrete linear ordered field (classical)
* [complete](complete.lean) : the reals are Cauchy complete (classical)