From 08fbf127c61ce164cbcd523d6f79a067e250b9bd Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Tue, 22 Dec 2015 13:25:38 -0500
Subject: [PATCH] feat(library/theories/analysis/metric_space,real_limit):
 define complete metric space, make real an instance

---
 library/theories/analysis/metric_space.lean | 10 +++++++++-
 library/theories/analysis/real_limit.lean   |  8 +++++++-
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean
index 3869ccfa7f..b04fa5c960 100644
--- a/library/theories/analysis/metric_space.lean
+++ b/library/theories/analysis/metric_space.lean
@@ -211,7 +211,8 @@ exists.intro δ (and.intro
      (suffices dist x x' < δ, from and.right Hδ x' (and.intro Heq this),
       this)))
 
-theorem image_seq_converges_of_converges [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N} (Hf : continuous f) :
+theorem image_seq_converges_of_converges [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N}
+                                                    (Hf : continuous f) :
         converges_seq (λ n, f (X n)) :=
   begin
     cases HX with xlim Hxlim,
@@ -236,3 +237,10 @@ theorem image_seq_converges_of_converges [instance] (X : ℕ → M) [HX : conver
 end metric_space_M_N
 
 end metric_space
+
+/- complete metric spaces -/
+
+open metric_space
+
+structure complete_metric_space [class] (M : Type) extends metricM : metric_space M : Type :=
+(complete : ∀ X, @cauchy M metricM X → @converges_seq M metricM X)
diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean
index 1eee0bd4e0..252c20fa10 100644
--- a/library/theories/analysis/real_limit.lean
+++ b/library/theories/analysis/real_limit.lean
@@ -28,7 +28,7 @@ namespace real
 local postfix ⁻¹ := pnat.inv
 /- the reals form a metric space -/
 
-protected definition to_metric_space [instance] : metric_space ℝ :=
+protected definition metric_space [instance] : metric_space ℝ :=
 ⦃ metric_space,
   dist               := λ x y, abs (x - y),
   dist_self          := λ x, abstract by rewrite [sub_self, abs_zero] end,
@@ -169,6 +169,12 @@ exists.intro l
         have abs (X n - l) ≤ real.of_rat k⁻¹, by apply conv k n' Hn,
         show abs (X n - l) < ε, from lt_of_le_of_lt this Hk))
 
+protected definition complete_metric_space [reducible] [trans_instance] :
+    complete_metric_space ℝ :=
+⦃complete_metric_space, real.metric_space,
+  complete := @converges_seq_of_cauchy
+⦄
+
 open set
 
 private definition exists_is_sup {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) :