fix(analysis/metric_space): rename continuous_of_metric to continuous…

…_iff_metric

analysis/complex.lean

@@ -24,12 +24,12 @@ instance : metric_space ℂ :=
 theorem dist_eq (x y : ℂ) : dist x y = (x - y).abs := rfl
 
 theorem uniform_continuous_add : uniform_continuous (λp : ℂ × ℂ, p.1 + p.2) :=
-uniform_continuous_of_metric.2 $ λ ε ε0,
+uniform_continuous_iff_metric.2 $ λ ε ε0,
 let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abs ε0 in
 ⟨δ, δ0, λ a b h, let ⟨h₁, h₂⟩ := max_lt_iff.1 h in Hδ h₁ h₂⟩
 
 theorem uniform_continuous_neg : uniform_continuous (@has_neg.neg ℂ _) :=
-uniform_continuous_of_metric.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
+uniform_continuous_iff_metric.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
   by rw dist_comm at h; simpa [dist_eq] using h⟩
 
 instance : uniform_add_group ℂ :=
@@ -39,12 +39,12 @@ instance : topological_add_group ℂ := by apply_instance
 
 lemma uniform_continuous_inv (s : set ℂ) {r : ℝ} (r0 : 0 < r) (H : ∀ x ∈ s, r ≤ abs x) :
   uniform_continuous (λp:s, p.1⁻¹) :=
-uniform_continuous_of_metric.2 $ λ ε ε0,
+uniform_continuous_iff_metric.2 $ λ ε ε0,
 let ⟨δ, δ0, Hδ⟩ := rat_inv_continuous_lemma abs ε0 r0 in
 ⟨δ, δ0, λ a b h, Hδ (H _ a.2) (H _ b.2) h⟩
 
 lemma uniform_continuous_abs : uniform_continuous (abs : ℂ → ℝ) :=
-uniform_continuous_of_metric.2 $ λ ε ε0,
+uniform_continuous_iff_metric.2 $ λ ε ε0,
   ⟨ε, ε0, λ a b, lt_of_le_of_lt (abs_abs_sub_le_abs_sub _ _)⟩
 
 lemma continuous_abs : continuous (abs : ℂ → ℝ) :=
@@ -66,7 +66,7 @@ show continuous ((has_inv.inv ∘ @subtype.val ℂ (λr, r ≠ 0)) ∘ λa, ⟨f
   from (continuous_subtype_mk _ hf).comp continuous_inv'
 
 lemma uniform_continuous_mul_const {x : ℂ} : uniform_continuous ((*) x) :=
-uniform_continuous_of_metric.2 $ λ ε ε0, begin
+uniform_continuous_iff_metric.2 $ λ ε ε0, begin
   cases no_top (abs x) with y xy,
   have y0 := lt_of_le_of_lt (abs_nonneg _) xy,
   refine ⟨_, div_pos ε0 y0, λ a b h, _⟩,
@@ -78,7 +78,7 @@ lemma uniform_continuous_mul (s : set (ℂ × ℂ))
   {r₁ r₂ : ℝ} (r₁0 : 0 < r₁) (r₂0 : 0 < r₂)
   (H : ∀ x ∈ s, abs (x : ℂ × ℂ).1 < r₁ ∧ abs x.2 < r₂) :
   uniform_continuous (λp:s, p.1.1 * p.1.2) :=
-uniform_continuous_of_metric.2 $ λ ε ε0,
+uniform_continuous_iff_metric.2 $ λ ε ε0,
 let ⟨δ, δ0, Hδ⟩ := rat_mul_continuous_lemma abs ε0 r₁0 r₂0 in
 ⟨δ, δ0, λ a b h,
   let ⟨h₁, h₂⟩ := max_lt_iff.1 h in Hδ (H _ a.2).1 (H _ b.2).2 h₁ h₂⟩
@@ -100,17 +100,17 @@ tendsto_of_uniform_continuous_subtype
 local attribute [semireducible] real.le
 
 lemma uniform_continuous_re : uniform_continuous re :=
-uniform_continuous_of_metric.2 (λ ε ε0, ⟨ε, ε0, λ _ _, lt_of_le_of_lt (abs_re_le_abs _)⟩)
+uniform_continuous_iff_metric.2 (λ ε ε0, ⟨ε, ε0, λ _ _, lt_of_le_of_lt (abs_re_le_abs _)⟩)
 
 lemma continuous_re : continuous re := uniform_continuous_re.continuous
 
 lemma uniform_continuous_im : uniform_continuous im :=
-uniform_continuous_of_metric.2 (λ ε ε0, ⟨ε, ε0, λ _ _, lt_of_le_of_lt (abs_im_le_abs _)⟩)
+uniform_continuous_iff_metric.2 (λ ε ε0, ⟨ε, ε0, λ _ _, lt_of_le_of_lt (abs_im_le_abs _)⟩)
 
 lemma continuous_im : continuous im := uniform_continuous_im.continuous
 
 lemma uniform_continuous_of_real : uniform_continuous of_real :=
-uniform_continuous_of_metric.2 (λ ε ε0, ⟨ε, ε0, λ _ _,
+uniform_continuous_iff_metric.2 (λ ε ε0, ⟨ε, ε0, λ _ _,
   by rw [real.dist_eq, complex.dist_eq, of_real_eq_coe, of_real_eq_coe, ← of_real_sub, abs_of_real];
     exact id⟩)
 

analysis/metric_space.lean

@@ -251,7 +251,7 @@ theorem dist_mem_uniformity {ε:ℝ} (ε0 : 0 < ε) :
   {p:α×α | dist p.1 p.2 < ε} ∈ (@uniformity α _).sets :=
 mem_uniformity_dist.2 ⟨ε, ε0, λ a b, id⟩
 
-theorem uniform_continuous_of_metric [metric_space β] {f : α → β} :
+theorem uniform_continuous_iff_metric [metric_space β] {f : α → β} :
   uniform_continuous f ↔ ∀ ε > 0, ∃ δ > 0,
     ∀{a b:α}, dist a b < δ → dist (f a) (f b) < ε :=
 uniform_continuous_def.trans
@@ -324,15 +324,15 @@ theorem tendsto_nhds_of_metric [metric_space β] {f : α → β} {a b} :
   let ⟨ε, ε0, hε⟩ := mem_nhds_iff_metric.1 hs, ⟨δ, δ0, hδ⟩ := H _ ε0 in
   mem_nhds_iff_metric.2 ⟨δ, δ0, λ x h, hε (hδ h)⟩⟩
 
-theorem continuous_of_metric [metric_space β] {f : α → β} :
+theorem continuous_iff_metric [metric_space β] {f : α → β} :
   continuous f ↔
     ∀b (ε > 0), ∃ δ > 0, ∀a, dist a b < δ → dist (f a) (f b) < ε :=
 continuous_iff_tendsto.trans $ forall_congr $ λ b, tendsto_nhds_of_metric
 
 theorem exists_delta_of_continuous [metric_space β] {f : α → β} {ε : ℝ}
   (hf : continuous f) (hε : ε > 0) (b : α) :
   ∃ δ > 0, ∀a, dist a b ≤ δ → dist (f a) (f b) < ε :=
-let ⟨δ, δ_pos, hδ⟩ := continuous_of_metric.1 hf b ε hε in
+let ⟨δ, δ_pos, hδ⟩ := continuous_iff_metric.1 hf b ε hε in
 ⟨δ / 2, half_pos δ_pos, assume a ha, hδ a $ lt_of_le_of_lt ha $ div_two_lt_of_pos δ_pos⟩
 
 theorem tendsto_nhds_topo_metric {f : filter β} {u : β → α} {a : α} :
@@ -586,7 +586,7 @@ instance prod.metric_space_max [metric_space β] : metric_space (α × β) :=
   to_uniform_space := prod.uniform_space }
 
 theorem uniform_continuous_dist' : uniform_continuous (λp:α×α, dist p.1 p.2) :=
-uniform_continuous_of_metric.2 (λ ε ε0, ⟨ε/2, half_pos ε0,
+uniform_continuous_iff_metric.2 (λ ε ε0, ⟨ε/2, half_pos ε0,
 begin
   suffices,
   { intros p q h, cases p with p₁ p₂, cases q with q₁ q₂,

analysis/real.lean

@@ -64,7 +64,7 @@ theorem embedding_of_rat : embedding (coe : ℚ → ℝ) := dense_embedding_of_r
 theorem continuous_of_rat : continuous (coe : ℚ → ℝ) := uniform_continuous_of_rat.continuous
 
 theorem real.uniform_continuous_add : uniform_continuous (λp : ℝ × ℝ, p.1 + p.2) :=
-uniform_continuous_of_metric.2 $ λ ε ε0,
+uniform_continuous_iff_metric.2 $ λ ε ε0,
 let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abs ε0 in
 ⟨δ, δ0, λ a b h, let ⟨h₁, h₂⟩ := max_lt_iff.1 h in Hδ h₁ h₂⟩
 
@@ -75,11 +75,11 @@ uniform_embedding_of_rat.uniform_continuous_iff.2 $ by simp [(∘)]; exact
   (uniform_continuous_snd.comp uniform_continuous_of_rat)).comp real.uniform_continuous_add
 
 theorem real.uniform_continuous_neg : uniform_continuous (@has_neg.neg ℝ _) :=
-uniform_continuous_of_metric.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
+uniform_continuous_iff_metric.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
   by rw dist_comm at h; simpa [real.dist_eq] using h⟩
 
 theorem rat.uniform_continuous_neg : uniform_continuous (@has_neg.neg ℚ _) :=
-uniform_continuous_of_metric.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
+uniform_continuous_iff_metric.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
   by rw dist_comm at h; simpa [rat.dist_eq] using h⟩
 
 instance : uniform_add_group ℝ :=
@@ -120,19 +120,19 @@ _ -/
 
 lemma real.uniform_continuous_inv (s : set ℝ) {r : ℝ} (r0 : 0 < r) (H : ∀ x ∈ s, r ≤ abs x) :
   uniform_continuous (λp:s, p.1⁻¹) :=
-uniform_continuous_of_metric.2 $ λ ε ε0,
+uniform_continuous_iff_metric.2 $ λ ε ε0,
 let ⟨δ, δ0, Hδ⟩ := rat_inv_continuous_lemma abs ε0 r0 in
 ⟨δ, δ0, λ a b h, Hδ (H _ a.2) (H _ b.2) h⟩
 
 lemma real.uniform_continuous_abs : uniform_continuous (abs : ℝ → ℝ) :=
-uniform_continuous_of_metric.2 $ λ ε ε0,
+uniform_continuous_iff_metric.2 $ λ ε ε0,
   ⟨ε, ε0, λ a b, lt_of_le_of_lt (abs_abs_sub_abs_le_abs_sub _ _)⟩
 
 lemma real.continuous_abs : continuous (abs : ℝ → ℝ) :=
 real.uniform_continuous_abs.continuous
 
 lemma rat.uniform_continuous_abs : uniform_continuous (abs : ℚ → ℚ) :=
-uniform_continuous_of_metric.2 $ λ ε ε0,
+uniform_continuous_iff_metric.2 $ λ ε ε0,
   ⟨ε, ε0, λ a b h, lt_of_le_of_lt
     (by simpa [rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _) h⟩
 
@@ -155,7 +155,7 @@ show continuous ((has_inv.inv ∘ @subtype.val ℝ (λr, r ≠ 0)) ∘ λa, ⟨f
   from (continuous_subtype_mk _ hf).comp real.continuous_inv'
 
 lemma real.uniform_continuous_mul_const {x : ℝ} : uniform_continuous ((*) x) :=
-uniform_continuous_of_metric.2 $ λ ε ε0, begin
+uniform_continuous_iff_metric.2 $ λ ε ε0, begin
   cases no_top (abs x) with y xy,
   have y0 := lt_of_le_of_lt (abs_nonneg _) xy,
   refine ⟨_, div_pos ε0 y0, λ a b h, _⟩,
@@ -167,7 +167,7 @@ lemma real.uniform_continuous_mul (s : set (ℝ × ℝ))
   {r₁ r₂ : ℝ} (r₁0 : 0 < r₁) (r₂0 : 0 < r₂)
   (H : ∀ x ∈ s, abs (x : ℝ × ℝ).1 < r₁ ∧ abs x.2 < r₂) :
   uniform_continuous (λp:s, p.1.1 * p.1.2) :=
-uniform_continuous_of_metric.2 $ λ ε ε0,
+uniform_continuous_iff_metric.2 $ λ ε ε0,
 let ⟨δ, δ0, Hδ⟩ := rat_mul_continuous_lemma abs ε0 r₁0 r₂0 in
 ⟨δ, δ0, λ a b h,
   let ⟨h₁, h₂⟩ := max_lt_iff.1 h in Hδ (H _ a.2).1 (H _ b.2).2 h₁ h₂⟩