chore(topology/*): @uniformity α _ becomes 𝓤 α (#814)

This is a binder type change and a local notation

src/topology/algebra/infinite_sum.lean

@@ -452,7 +452,7 @@ lemma has_sum_iff_cauchy : has_sum f ↔ cauchy (map (λ (s : finset β), sum s
 (cauchy_map_iff_exists_tendsto at_top_ne_bot).symm
 
 lemma has_sum_iff_vanishing :
-  has_sum f ↔ ∀e∈(nhds (0:α)).sets, (∃s:finset β, ∀t, disjoint t s → t.sum f ∈ e) :=
+  has_sum f ↔ ∀ e ∈ nhds (0:α), (∃s:finset β, ∀t, disjoint t s → t.sum f ∈ e) :=
 begin
   simp only [has_sum_iff_cauchy, cauchy_map_iff, and_iff_right at_top_ne_bot,
     prod_at_top_at_top_eq, uniformity_eq_comap_nhds_zero α, tendsto_comap_iff, (∘)],

src/topology/algebra/uniform_group.lean

@@ -18,6 +18,7 @@ import topology.uniform_space.uniform_embedding topology.uniform_space.separatio
 noncomputable theory
 local attribute [instance, priority 0] classical.prop_decidable
 
+local notation `𝓤` := uniformity
 
 section uniform_add_group
 open filter set
@@ -74,13 +75,13 @@ instance [uniform_space β] [add_group β] [uniform_add_group β] : uniform_add_
     (uniform_continuous_fst.comp uniform_continuous_snd)
     (uniform_continuous_snd.comp uniform_continuous_snd)) ⟩
 
-lemma uniformity_translate (a : α) : uniformity.map (λx:α×α, (x.1 + a, x.2 + a)) = uniformity :=
+lemma uniformity_translate (a : α) : (𝓤 α).map (λx:α×α, (x.1 + a, x.2 + a)) = 𝓤 α :=
 le_antisymm
   (uniform_continuous_add uniform_continuous_id uniform_continuous_const)
-  (calc uniformity =
-    (uniformity.map (λx:α×α, (x.1 + -a, x.2 + -a))).map (λx:α×α, (x.1 + a, x.2 + a)) :
+  (calc 𝓤 α =
+    ((𝓤 α).map (λx:α×α, (x.1 + -a, x.2 + -a))).map (λx:α×α, (x.1 + a, x.2 + a)) :
       by simp [filter.map_map, (∘)]; exact filter.map_id.symm
-    ... ≤ uniformity.map (λx:α×α, (x.1 + a, x.2 + a)) :
+    ... ≤ (𝓤 α).map (λx:α×α, (x.1 + a, x.2 + a)) :
       filter.map_mono (uniform_continuous_add uniform_continuous_id uniform_continuous_const))
 
 lemma uniform_embedding_translate (a : α) : uniform_embedding (λx:α, x + a) :=
@@ -93,7 +94,7 @@ end
 
 section
 variables (α)
-lemma uniformity_eq_comap_nhds_zero : uniformity = comap (λx:α×α, x.2 - x.1) (nhds (0:α)) :=
+lemma uniformity_eq_comap_nhds_zero : 𝓤 α = comap (λx:α×α, x.2 - x.1) (nhds (0:α)) :=
 begin
   rw [nhds_eq_comap_uniformity, filter.comap_comap_comp],
   refine le_antisymm (filter.map_le_iff_le_comap.1 _) _,
@@ -111,7 +112,7 @@ end
 
 lemma group_separation_rel (x y : α) : (x, y) ∈ separation_rel α ↔ x - y ∈ closure ({0} : set α) :=
 have embedding (λa, a + (y - x)), from (uniform_embedding_translate (y - x)).embedding,
-show (x, y) ∈ ⋂₀ uniformity.sets ↔ x - y ∈ closure ({0} : set α),
+show (x, y) ∈ ⋂₀ (𝓤 α).sets ↔ x - y ∈ closure ({0} : set α),
 begin
   rw [this.closure_eq_preimage_closure_image, uniformity_eq_comap_nhds_zero α, sInter_comap_sets],
   simp [mem_closure_iff_nhds, inter_singleton_eq_empty]
@@ -192,7 +193,7 @@ def topological_add_group.to_uniform_space : uniform_space G :=
 section
 local attribute [instance] topological_add_group.to_uniform_space
 
-lemma uniformity_eq_comap_nhds_zero' : uniformity = comap (λp:G×G, p.2 - p.1) (nhds (0 : G)) := rfl
+lemma uniformity_eq_comap_nhds_zero' : 𝓤 G = comap (λp:G×G, p.2 - p.1) (nhds (0 : G)) := rfl
 
 variable {G}
 lemma topological_add_group_is_uniform : uniform_add_group G :=
@@ -213,7 +214,7 @@ lemma to_uniform_space_eq {α : Type*} [u : uniform_space α] [add_comm_group α
   topological_add_group.to_uniform_space α = u :=
 begin
   ext : 1,
-  show @uniformity α (topological_add_group.to_uniform_space α) = uniformity,
+  show @uniformity α (topological_add_group.to_uniform_space α) = 𝓤 α,
   rw [uniformity_eq_comap_nhds_zero' α, uniformity_eq_comap_nhds_zero α]
 end
 

src/topology/metric_space/basic.lean

@@ -13,6 +13,8 @@ import data.real.nnreal topology.metric_space.emetric_space topology.algebra.ord
 open lattice set filter classical topological_space
 noncomputable theory
 
+local notation `𝓤` := uniformity
+
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
@@ -63,7 +65,7 @@ class metric_space (α : Type u) extends has_dist α : Type u :=
 (edist : α → α → ennreal := λx y, ennreal.of_real (dist x y))
 (edist_dist : ∀ x y : α, edist x y = ennreal.of_real (dist x y) . control_laws_tac)
 (to_uniform_space : uniform_space α := uniform_space_of_dist dist dist_self dist_comm dist_triangle)
-(uniformity_dist : uniformity = ⨅ ε>0, principal {p:α×α | dist p.1 p.2 < ε} . control_laws_tac)
+(uniformity_dist : 𝓤 α = ⨅ ε>0, principal {p:α×α | dist p.1 p.2 < ε} . control_laws_tac)
 
 variables [metric_space α]
 
@@ -248,14 +250,14 @@ theorem ball_eq_empty_iff_nonpos : ε ≤ 0 ↔ ball x ε = ∅ :=
 ⟨λ h, le_of_not_gt $ λ ε0, h _ $ mem_ball_self ε0,
  λ ε0 y h, not_lt_of_le ε0 $ pos_of_mem_ball h⟩).symm
 
-theorem uniformity_dist : uniformity = (⨅ ε>0, principal {p:α×α | dist p.1 p.2 < ε}) :=
+theorem uniformity_dist : 𝓤 α = (⨅ ε>0, principal {p:α×α | dist p.1 p.2 < ε}) :=
 metric_space.uniformity_dist _
 
-theorem uniformity_dist' : uniformity = (⨅ε:{ε:ℝ // ε>0}, principal {p:α×α | dist p.1 p.2 < ε.val}) :=
+theorem uniformity_dist' : 𝓤 α = (⨅ε:{ε:ℝ // ε>0}, principal {p:α×α | dist p.1 p.2 < ε.val}) :=
 by simp [infi_subtype]; exact uniformity_dist
 
 theorem mem_uniformity_dist {s : set (α×α)} :
-  s ∈ @uniformity α _ ↔ (∃ε>0, ∀{a b:α}, dist a b < ε → (a, b) ∈ s) :=
+  s ∈ 𝓤 α ↔ (∃ε>0, ∀{a b:α}, dist a b < ε → (a, b) ∈ s) :=
 begin
   rw [uniformity_dist', mem_infi],
   simp [subset_def],
@@ -264,7 +266,7 @@ begin
 end
 
 theorem dist_mem_uniformity {ε:ℝ} (ε0 : 0 < ε) :
-  {p:α×α | dist p.1 p.2 < ε} ∈ @uniformity α _ :=
+  {p:α×α | dist p.1 p.2 < ε} ∈ 𝓤 α :=
 mem_uniformity_dist.2 ⟨ε, ε0, λ a b, id⟩
 
 theorem uniform_continuous_iff [metric_space β] {f : α → β} :
@@ -399,7 +401,7 @@ distance coincide. -/
 
 /-- Expressing the uniformity in terms of `edist` -/
 protected lemma metric.mem_uniformity_edist {s : set (α×α)} :
-  s ∈ @uniformity α _ ↔ (∃ε>0, ∀{a b:α}, edist a b < ε → (a, b) ∈ s) :=
+  s ∈ 𝓤 α ↔ (∃ε>0, ∀{a b:α}, edist a b < ε → (a, b) ∈ s) :=
 begin
   refine mem_uniformity_dist.trans ⟨_, _⟩; rintro ⟨ε, ε0, Hε⟩,
   { refine ⟨ennreal.of_real ε, _, λ a b, _⟩,
@@ -412,7 +414,7 @@ begin
     rwa [edist_dist, ennreal.of_real_lt_of_real_iff ε0'] }
 end
 
-protected theorem metric.uniformity_edist' : uniformity = (⨅ε:{ε:ennreal // ε>0}, principal {p:α×α | edist p.1 p.2 < ε.val}) :=
+protected theorem metric.uniformity_edist' : 𝓤 α = (⨅ε:{ε:ennreal // ε>0}, principal {p:α×α | edist p.1 p.2 < ε.val}) :=
 begin
   ext s, rw mem_infi,
   { simp [metric.mem_uniformity_edist, subset_def] },
@@ -421,7 +423,7 @@ begin
   { exact ⟨⟨1, ennreal.zero_lt_one⟩⟩ }
 end
 
-theorem uniformity_edist : uniformity = (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}) :=
+theorem uniformity_edist : 𝓤 α = (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}) :=
 by simpa [infi_subtype] using @metric.uniformity_edist' α _
 
 /-- A metric space induces an emetric space -/
@@ -528,7 +530,7 @@ begin
 end
 
 theorem metric.uniformity_eq_comap_nhds_zero :
-  uniformity = comap (λp:α×α, dist p.1 p.2) (nhds (0 : ℝ)) :=
+  𝓤 α = comap (λp:α×α, dist p.1 p.2) (nhds (0 : ℝ)) :=
 begin
   simp only [uniformity_dist', nhds_eq, comap_infi, comap_principal],
   congr, funext ε,

src/topology/metric_space/cau_seq_filter.lean

@@ -394,7 +394,6 @@ begin
       apply hεs,
       rw dist_eq_norm,
       apply hN; assumption }},
-  { apply_instance }
 end
 
 /-- In a normed field, `cau_seq` coincides with the usual notion of Cauchy sequences. -/

src/topology/metric_space/emetric_space.lean

@@ -21,6 +21,8 @@ import topology.uniform_space.separation topology.uniform_space.uniform_embeddin
 open lattice set filter classical
 noncomputable theory
 
+local notation `𝓤` := uniformity
+
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
@@ -100,7 +102,7 @@ class emetric_space (α : Type u) extends has_edist α : Type u :=
 (edist_comm : ∀ x y : α, edist x y = edist y x)
 (edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z)
 (to_uniform_space : uniform_space α := uniform_space_of_edist edist edist_self edist_comm edist_triangle)
-(uniformity_edist : uniformity = ⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε} . control_laws_tac)
+(uniformity_edist : 𝓤 α = ⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε} . control_laws_tac)
 
 /- emetric spaces are less common than metric spaces. Therefore, we work in a dedicated
 namespace, while notions associated to metric spaces are mostly in the root namespace. -/
@@ -139,15 +141,15 @@ theorem eq_of_forall_edist_le {x y : α} (h : ∀ε, ε > 0 → edist x y ≤ ε
 eq_of_edist_eq_zero (eq_of_le_of_forall_le_of_dense (by simp) h)
 
 /-- Reformulation of the uniform structure in terms of the extended distance -/
-theorem uniformity_edist' : uniformity = (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}) :=
+theorem uniformity_edist' : 𝓤 α = (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}) :=
 emetric_space.uniformity_edist _
 
 /-- Reformulation of the uniform structure in terms of the extended distance on a subtype -/
-theorem uniformity_edist'' : uniformity = (⨅ε:{ε:ennreal // ε>0}, principal {p:α×α | edist p.1 p.2 < ε.val}) :=
+theorem uniformity_edist'' : 𝓤 α = (⨅ε:{ε:ennreal // ε>0}, principal {p:α×α | edist p.1 p.2 < ε.val}) :=
 by simp [infi_subtype]; exact uniformity_edist'
 
 theorem uniformity_edist_nnreal :
-  uniformity = (⨅(ε:nnreal) (h : ε > 0), principal {p:α×α | edist p.1 p.2 < ε}) :=
+  𝓤 α = (⨅(ε:nnreal) (h : ε > 0), principal {p:α×α | edist p.1 p.2 < ε}) :=
 begin
   rw [uniformity_edist', ennreal.infi_ennreal, inf_of_le_left],
   { congr, funext ε, refine infi_congr_Prop ennreal.coe_pos _, assume h, refl },
@@ -157,7 +159,7 @@ end
 
 /-- Characterization of the elements of the uniformity in terms of the extended distance -/
 theorem mem_uniformity_edist {s : set (α×α)} :
-  s ∈ @uniformity α _ ↔ (∃ε>0, ∀{a b:α}, edist a b < ε → (a, b) ∈ s) :=
+  s ∈ 𝓤 α ↔ (∃ε>0, ∀{a b:α}, edist a b < ε → (a, b) ∈ s) :=
 begin
   rw [uniformity_edist'', mem_infi],
   simp [subset_def],
@@ -167,7 +169,7 @@ end
 
 /-- Fixed size neighborhoods of the diagonal belong to the uniform structure -/
 theorem edist_mem_uniformity {ε:ennreal} (ε0 : 0 < ε) :
-  {p:α×α | edist p.1 p.2 < ε} ∈ @uniformity α _ :=
+  {p:α×α | edist p.1 p.2 < ε} ∈ 𝓤 α :=
 mem_uniformity_edist.2 ⟨ε, ε0, λ a b, id⟩
 
 namespace emetric