From ef982d9ad63a7575a131020e75bc6cf1eb571564 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Wed, 6 Apr 2016 16:44:29 -0400
Subject: [PATCH] refactor(library/theories/analysis/metric_space.lean): use
 new definition of continuous_at

---
 library/theories/analysis/metric_space.lean | 22 +++++++++------------
 library/theories/topology/basic.lean        | 17 ----------------
 library/theories/topology/continuous.lean   | 10 +++++-----
 3 files changed, 14 insertions(+), 35 deletions(-)

diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean
index ec45a736d..eb81196f9 100644
--- a/library/theories/analysis/metric_space.lean
+++ b/library/theories/analysis/metric_space.lean
@@ -5,7 +5,7 @@ Author: Jeremy Avigad
 
 Metric spaces.
 -/
-import data.real.complete data.pnat data.list.sort ..topology.basic data.set
+import data.real.complete data.pnat data.list.sort ..topology.continuous data.set
 open nat real eq.ops classical
 
 structure metric_space [class] (M : Type) : Type :=
@@ -667,26 +667,25 @@ theorem continuous_at_intro {f : M → N} {x : M}
         continuous_at f x :=
   begin
     rewrite ↑continuous_at,
-    intros U HfU Uopen,
+    intros U Uopen HfU,
     cases ex_Open_ball_subset_of_Open_of_nonempty Uopen HfU with r Hr,
     cases Hr with Hr HUr,
     cases H Hr with δ Hδ,
     cases Hδ with Hδ Hx'δ,
     existsi open_ball x δ,
     split,
+    apply open_ball_open,
+    split,
     apply mem_open_ball,
     exact Hδ,
-    split,
-    apply open_ball_open,
     intro y Hy,
+    apply mem_preimage,
     apply HUr,
     cases Hy with y' Hy',
-    cases Hy' with Hy' Hfy',
-    cases Hy' with _ Hy',
     rewrite dist_comm at Hy',
     note Hy'' := Hx'δ Hy',
     apply and.intro !mem_univ,
-    rewrite [-Hfy', dist_comm],
+    rewrite dist_comm,
     exact Hy''
   end
 
@@ -695,9 +694,9 @@ theorem continuous_at_elim {f : M → N} {x : M} (Hfx : continuous_at f x) :
   begin
     intros ε Hε,
     rewrite [↑continuous_at at Hfx],
-    cases Hfx (open_ball (f x) ε) (mem_open_ball _ Hε) !open_ball_open with V HV,
-    cases HV with HVx HV,
-    cases HV with HV HVf,
+    cases @Hfx (open_ball (f x) ε) !open_ball_open (mem_open_ball _ Hε) with V HV,
+    cases HV with HV HVx,
+    cases HVx with HVx HVf,
     cases ex_Open_ball_subset_of_Open_of_nonempty HV HVx with δ Hδ,
     cases Hδ with Hδ Hδx,
     existsi δ,
@@ -707,13 +706,10 @@ theorem continuous_at_elim {f : M → N} {x : M} (Hfx : continuous_at f x) :
     rewrite dist_comm,
     apply and.right,
     apply HVf,
-    existsi x',
-    split,
     apply Hδx,
     apply and.intro !mem_univ,
     rewrite dist_comm,
     apply Hx',
-    apply rfl
   end
 
 theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x at x) :
diff --git a/library/theories/topology/basic.lean b/library/theories/topology/basic.lean
index bce954e2a..ee4b3c228 100644
--- a/library/theories/topology/basic.lean
+++ b/library/theories/topology/basic.lean
@@ -284,23 +284,6 @@ theorem topology_generated_by_initial {X : Type} {B : set (set X)} {T : topology
   @Open _ T s :=
 opens_generated_by_initial H H1
 
-section continuity
-
-/- continuous mappings -/
-/- continuity at a point -/
-
-variables {M N : Type} [Tm : topology M] [Tn : topology N]
-include Tm Tn
-
-definition continuous_at (f : M → N) (x : M) :=
-  ∀ U : set N, f x ∈ U → Open U → ∃ V : set M, x ∈ V ∧ Open V ∧ f 'V ⊆ U
-
-/-
-definition continuous (f : M → N) :=
-  ∀ x : M, continuous_at f x
--/
-end continuity
-
 section boundary
 variables {X : Type} [TX : topology X]
 include TX
diff --git a/library/theories/topology/continuous.lean b/library/theories/topology/continuous.lean
index fc906010d..1c59f6f6b 100644
--- a/library/theories/topology/continuous.lean
+++ b/library/theories/topology/continuous.lean
@@ -243,12 +243,12 @@ continuous_of_continuous_on_univ (continuous_on_const c univ)
 
 /- continuity at a point -/
 
-definition continuous_at' (f : X → Y) (x : X) : Prop :=
+definition continuous_at (f : X → Y) (x : X) : Prop :=
 ∀ ⦃t : set Y⦄, Open t → f x ∈ t → ∃ u, Open u ∧ x ∈ u ∧ u ⊆ f '- t
 
 theorem continuous_at_of_continuous_at_on {f : X → Y} {x : X} {s : set X}
     (Os : Open s) (xs : x ∈ s) (H : continuous_at_on f x s) :
-  continuous_at' f x :=
+  continuous_at f x :=
 take t, assume Ot fxt,
 obtain u Ou xu xssub, from H Ot fxt,
 exists.intro (u ∩ s) (and.intro (Open_inter Ou Os)
@@ -256,11 +256,11 @@ exists.intro (u ∩ s) (and.intro (Open_inter Ou Os)
 
 theorem continuous_at_of_continuous_at_on_univ {f : X → Y} {x : X}
     (H : continuous_at_on f x univ) :
-  continuous_at' f x :=
+  continuous_at f x :=
 continuous_at_of_continuous_at_on Open_univ !mem_univ H
 
 theorem continuous_at_on_univ_of_continuous_at {f : X → Y} {x : X}
-    (H : continuous_at' f x) :
+    (H : continuous_at f x) :
   continuous_at_on f x univ :=
 take t, assume Ot fxt,
 obtain u Ou xu usub, from H Ot fxt,
@@ -268,7 +268,7 @@ have u ∩ univ ⊆ f '- t, by rewrite inter_univ; apply usub,
 exists.intro u (and.intro Ou (and.intro xu this))
 
 theorem continuous_at_iff_continuous_at_on_univ (f : X → Y) (x : X) :
-  continuous_at' f x ↔ continuous_at_on f x univ :=
+  continuous_at f x ↔ continuous_at_on f x univ :=
 iff.intro continuous_at_on_univ_of_continuous_at continuous_at_of_continuous_at_on_univ