From b1aea149dbfa2ad1cb4c5f425cec2f653fab299d Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 9 Jun 2015 15:43:43 +1000 Subject: [PATCH] chore(library/data/real): update md --- library/data/real/real.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/library/data/real/real.md b/library/data/real/real.md index 2acde23a7..5e05818fd 100644 --- a/library/data/real/real.md +++ b/library/data/real/real.md @@ -1,8 +1,9 @@ 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) * [order](order.lean) : the reals as an ordered ring (constructive) -* [division](division.lean) : the reals as a discrete linear ordered field (classical) \ No newline at end of file +* [division](division.lean) : the reals as a discrete linear ordered field (classical) +* [complete](complete.lean) : the reals are Cauchy complete (classical) \ No newline at end of file