feat(library/theories/analysis/metric_space,real_limit): define complete metric space, make real an instance

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)

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)) :