refactor(topology/*): add uniform_space.of_fun, use it (#18495)

* Fix `simps` config for `absolute_value`.
* Define `uniform_space.of_fun` and use it for `absolute_value.uniform_space`, `pseudo_emetric_space`, and `pseudo_metric_space`.
* Add `filter.tendsto_infi_infi` and `filter.tendsto_supr_supr`.
* Rename `pseudo_metric_space.of_metrizable` and `metric_space.of_metrizable` to `*.of_dist_topology`.
* Add `metric.to_uniform_space_eq` and `metric.uniformity_basis_dist_rat`.
* Migrate `topology.uniform_space.absolute_value` to bundled `absolute_value`.

Author: urkud

src/algebra/order/absolute_value.lean

@@ -39,8 +39,6 @@ namespace absolute_value
 
 attribute [nolint doc_blame] absolute_value.to_mul_hom
 
-initialize_simps_projections absolute_value (to_mul_hom_to_fun → apply)
-
 section ordered_semiring
 
 section semiring
@@ -68,6 +66,11 @@ instance subadditive_hom_class : subadditive_hom_class (absolute_value R S) R S
 
 @[ext] lemma ext ⦃f g : absolute_value R S⦄ : (∀ x, f x = g x) → f = g := fun_like.ext _ _
 
+/-- See Note [custom simps projection]. -/
+def simps.apply (f : absolute_value R S) : R → S := f
+
+initialize_simps_projections absolute_value (to_mul_hom_to_fun → apply)
+
 /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
 directly. -/
 instance : has_coe_to_fun (absolute_value R S) (λ f, R → S) := fun_like.has_coe_to_fun

src/order/filter/basic.lean

@@ -2531,6 +2531,10 @@ lemma tendsto_infi' {f : α → β} {x : ι → filter α} {y : filter β} (i :
   tendsto f (⨅ i, x i) y :=
 hi.mono_left $ infi_le _ _
 
+theorem tendsto_infi_infi {f : α → β} {x : ι → filter α} {y : ι → filter β}
+  (h : ∀ i, tendsto f (x i) (y i)) : tendsto f (infi x) (infi y) :=
+tendsto_infi.2 $ λ i, tendsto_infi' i (h i)
+
 @[simp] lemma tendsto_sup {f : α → β} {x₁ x₂ : filter α} {y : filter β} :
   tendsto f (x₁ ⊔ x₂) y ↔ tendsto f x₁ y ∧ tendsto f x₂ y :=
 by simp only [tendsto, map_sup, sup_le_iff]
@@ -2543,6 +2547,10 @@ lemma tendsto.sup {f : α → β} {x₁ x₂ : filter α} {y : filter β} :
   tendsto f (⨆ i, x i) y ↔ ∀ i, tendsto f (x i) y :=
 by simp only [tendsto, map_supr, supr_le_iff]
 
+theorem tendsto_supr_supr {f : α → β} {x : ι → filter α} {y : ι → filter β}
+  (h : ∀ i, tendsto f (x i) (y i)) : tendsto f (supr x) (supr y) :=
+tendsto_supr.2 $ λ i, (h i).mono_right $ le_supr _ _
+
 @[simp] lemma tendsto_principal {f : α → β} {l : filter α} {s : set β} :
   tendsto f l (𝓟 s) ↔ ∀ᶠ a in l, f a ∈ s :=
 by simp only [tendsto, le_principal_iff, mem_map', filter.eventually]

src/topology/metric_space/basic.lean

@@ -54,35 +54,14 @@ open_locale uniformity topology big_operators filter nnreal ennreal
 universes u v w
 variables {α : Type u} {β : Type v} {X ι : Type*}
 
-/-- Construct a uniform structure core from a distance function and metric space axioms.
-This is a technical construction that can be immediately used to construct a uniform structure
-from a distance function and metric space axioms but is also useful when discussing
-metrizable topologies, see `pseudo_metric_space.of_metrizable`. -/
-def uniform_space.core_of_dist {α : Type*} (dist : α → α → ℝ)
-  (dist_self : ∀ x : α, dist x x = 0)
-  (dist_comm : ∀ x y : α, dist x y = dist y x)
-  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : uniform_space.core α :=
-{ uniformity := (⨅ ε>0, 𝓟 {p:α×α | dist p.1 p.2 < ε}),
-  refl       := le_infi $ assume ε, le_infi $
-    by simp [set.subset_def, id_rel, dist_self, (>)] {contextual := tt},
-  comp       := le_infi $ assume ε, le_infi $ assume h, lift'_le
-    (mem_infi_of_mem (ε / 2) $ mem_infi_of_mem (div_pos h zero_lt_two) (subset.refl _)) $
-    have ∀ (a b c : α), dist a c < ε / 2 → dist c b < ε / 2 → dist a b < ε,
-      from assume a b c hac hcb,
-      calc dist a b ≤ dist a c + dist c b : dist_triangle _ _ _
-        ... < ε / 2 + ε / 2 : add_lt_add hac hcb
-        ... = ε : by rw [div_add_div_same, add_self_div_two],
-    by simpa [comp_rel],
-  symm       := tendsto_infi.2 $ assume ε, tendsto_infi.2 $ assume h,
-    tendsto_infi' ε $ tendsto_infi' h $ tendsto_principal_principal.2 $ by simp [dist_comm] }
-
 /-- Construct a uniform structure from a distance function and metric space axioms -/
 def uniform_space_of_dist
   (dist : α → α → ℝ)
   (dist_self : ∀ x : α, dist x x = 0)
   (dist_comm : ∀ x y : α, dist x y = dist y x)
   (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : uniform_space α :=
-uniform_space.of_core (uniform_space.core_of_dist dist dist_self dist_comm dist_triangle)
+uniform_space.of_fun dist dist_self dist_comm dist_triangle $ λ ε ε0,
+  ⟨ε / 2, half_pos ε0, λ x hx y hy, add_halves ε ▸ add_lt_add hx hy⟩
 
 /-- This is an internal lemma used to construct a bornology from a metric in `bornology.of_dist`. -/
 private lemma bounded_iff_aux {α : Type*} (dist : α → α → ℝ)
@@ -202,7 +181,7 @@ instance pseudo_metric_space.to_has_edist : has_edist α := ⟨pseudo_metric_spa
 /-- Construct a pseudo-metric space structure whose underlying topological space structure
 (definitionally) agrees which a pre-existing topology which is compatible with a given distance
 function. -/
-def pseudo_metric_space.of_metrizable {α : Type*} [topological_space α] (dist : α → α → ℝ)
+def pseudo_metric_space.of_dist_topology {α : Type u} [topological_space α] (dist : α → α → ℝ)
   (dist_self : ∀ x : α, dist x x = 0)
   (dist_comm : ∀ x y : α, dist x y = dist y x)
   (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
@@ -212,26 +191,11 @@ def pseudo_metric_space.of_metrizable {α : Type*} [topological_space α] (dist
   dist_self := dist_self,
   dist_comm := dist_comm,
   dist_triangle := dist_triangle,
-  to_uniform_space := { is_open_uniformity := begin
-    dsimp only [uniform_space.core_of_dist],
-    intros s,
-    change is_open s ↔ _,
-    rw H s,
-    refine forall₂_congr (λ x x_in, _),
-    erw (has_basis_binfi_principal _ nonempty_Ioi).mem_iff,
-    { refine exists₂_congr (λ ε ε_pos, _),
-      simp only [prod.forall, set_of_subset_set_of],
-      split,
-      { rintros h _ y H rfl,
-        exact h y H },
-      { intros h y hxy,
-        exact h _ _ hxy rfl } },
-    { exact λ r (hr : 0 < r) p (hp : 0 < p), ⟨min r p, lt_min hr hp,
-      λ x (hx : dist _ _ < _), lt_of_lt_of_le hx (min_le_left r p),
-      λ x (hx : dist _ _ < _), lt_of_lt_of_le hx (min_le_right r p)⟩ },
-    { apply_instance }
-    end,
-    ..uniform_space.core_of_dist dist dist_self dist_comm dist_triangle },
+  to_uniform_space :=
+  { is_open_uniformity := λ s, (H s).trans $ forall₂_congr $ λ x _,
+      ((uniform_space.has_basis_of_fun (exists_gt (0 : ℝ))
+        dist _ _ _ _).comap (prod.mk x)).mem_iff.symm.trans mem_comap_prod_mk,
+    to_core := (uniform_space_of_dist dist dist_self dist_comm dist_triangle).to_core },
   uniformity_dist := rfl,
   to_bornology := bornology.of_dist dist dist_self dist_comm dist_triangle,
   cobounded_sets := rfl }
@@ -653,14 +617,15 @@ theorem is_bounded_iff_nndist {s : set α} :
 by simp only [is_bounded_iff_exists_ge 0, nnreal.exists, ← nnreal.coe_le_coe, ← dist_nndist,
   nnreal.coe_mk, exists_prop]
 
+theorem to_uniform_space_eq : ‹pseudo_metric_space α›.to_uniform_space =
+  uniform_space_of_dist dist dist_self dist_comm dist_triangle :=
+uniform_space_eq pseudo_metric_space.uniformity_dist
+
 theorem uniformity_basis_dist :
   (𝓤 α).has_basis (λ ε : ℝ, 0 < ε) (λ ε, {p:α×α | dist p.1 p.2 < ε}) :=
 begin
-  rw ← pseudo_metric_space.uniformity_dist.symm,
-  refine has_basis_binfi_principal _ nonempty_Ioi,
-  exact λ r (hr : 0 < r) p (hp : 0 < p), ⟨min r p, lt_min hr hp,
-     λ x (hx : dist _ _ < _), lt_of_lt_of_le hx (min_le_left r p),
-     λ x (hx : dist _ _ < _), lt_of_lt_of_le hx (min_le_right r p)⟩
+  rw [to_uniform_space_eq],
+  exact uniform_space.has_basis_of_fun (exists_gt _) _ _ _ _ _
 end
 
 /-- Given `f : β → ℝ`, if `f` sends `{i | p i}` to a set of positive numbers
@@ -680,6 +645,11 @@ begin
   { exact λ ⟨i, hi, H⟩, ⟨f i, hf₀ i hi, H⟩ }
 end
 
+theorem uniformity_basis_dist_rat :
+  (𝓤 α).has_basis (λ r : ℚ, 0 < r) (λ r, {p : α × α | dist p.1 p.2 < r}) :=
+metric.mk_uniformity_basis (λ _, rat.cast_pos.2) $ λ ε hε,
+  let ⟨r, hr0, hrε⟩ := exists_rat_btwn hε in ⟨r, rat.cast_pos.1 hr0, hrε.le⟩
+
 theorem uniformity_basis_dist_inv_nat_succ :
   (𝓤 α).has_basis (λ _, true) (λ n:ℕ, {p:α×α | dist p.1 p.2 < 1 / (↑n+1) }) :=
 metric.mk_uniformity_basis (λ n _, div_pos zero_lt_one $ nat.cast_add_one_pos n)
@@ -1476,11 +1446,7 @@ def pseudo_metric_space.induced {α β} (f : α → β)
   edist              := λ x y, edist (f x) (f y),
   edist_dist         := λ x y, edist_dist _ _,
   to_uniform_space   := uniform_space.comap f m.to_uniform_space,
-  uniformity_dist    := begin
-    apply @uniformity_dist_of_mem_uniformity _ _ _ _ _ (λ x y, dist (f x) (f y)),
-    refine compl_surjective.forall.2 (λ s, compl_mem_comap.trans $ mem_uniformity_dist.trans _),
-    simp only [mem_compl_iff, @imp_not_comm _ (_ ∈ _), ← prod.forall', prod.mk.eta, ball_image_iff]
-  end,
+  uniformity_dist    := (uniformity_basis_dist.comap _).eq_binfi,
   to_bornology       := bornology.induced f,
   cobounded_sets     := set.ext $ compl_surjective.forall.2 $ λ s,
     by simp only [compl_mem_comap, filter.mem_sets, ← is_bounded_def, mem_set_of_eq, compl_compl,
@@ -2643,14 +2609,14 @@ end
 /-- Construct a metric space structure whose underlying topological space structure
 (definitionally) agrees which a pre-existing topology which is compatible with a given distance
 function. -/
-def metric_space.of_metrizable {α : Type*} [topological_space α] (dist : α → α → ℝ)
+def metric_space.of_dist_topology {α : Type u} [topological_space α] (dist : α → α → ℝ)
   (dist_self : ∀ x : α, dist x x = 0)
   (dist_comm : ∀ x y : α, dist x y = dist y x)
   (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
   (H : ∀ s : set α, is_open s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s)
   (eq_of_dist_eq_zero : ∀ x y : α, dist x y = 0 → x = y) : metric_space α :=
 { eq_of_dist_eq_zero := eq_of_dist_eq_zero,
-  ..pseudo_metric_space.of_metrizable dist dist_self dist_comm dist_triangle H }
+  ..pseudo_metric_space.of_dist_topology dist dist_self dist_comm dist_triangle H }
 
 variables {γ : Type w} [metric_space γ]
 

src/topology/metric_space/emetric_space.lean

@@ -38,41 +38,20 @@ variables {α : Type u} {β : Type v} {X : Type*}
 in terms of the elements of the uniformity. -/
 theorem uniformity_dist_of_mem_uniformity [linear_order β] {U : filter (α × α)} (z : β)
   (D : α → α → β) (H : ∀ s, s ∈ U ↔ ∃ε>z, ∀{a b:α}, D a b < ε → (a, b) ∈ s) :
-  U = ⨅ ε>z, 𝓟 {p:α×α | D p.1 p.2 < ε} :=
-le_antisymm
-  (le_infi $ λ ε, le_infi $ λ ε0, le_principal_iff.2 $ (H _).2 ⟨ε, ε0, λ a b, id⟩)
-  (λ r ur, let ⟨ε, ε0, h⟩ := (H _).1 ur in
-    mem_infi_of_mem ε $ mem_infi_of_mem ε0 $ mem_principal.2 $ λ ⟨a, b⟩, h)
+  U = ⨅ ε > z, 𝓟 {p:α×α | D p.1 p.2 < ε} :=
+has_basis.eq_binfi ⟨λ s, by simp only [H, subset_def, prod.forall, mem_set_of]⟩
 
 /-- `has_edist α` means that `α` is equipped with an extended distance. -/
 class has_edist (α : Type*) := (edist : α → α → ℝ≥0∞)
 export has_edist (edist)
 
 /-- Creating a uniform space from an extended distance. -/
-def uniform_space_of_edist
-  (edist : α → α → ℝ≥0∞)
-  (edist_self : ∀ x : α, edist x x = 0)
-  (edist_comm : ∀ x y : α, edist x y = edist y x)
+noncomputable def uniform_space_of_edist (edist : α → α → ℝ≥0∞)
+  (edist_self : ∀ x : α, edist x x = 0) (edist_comm : ∀ x y : α, edist x y = edist y x)
   (edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z) : uniform_space α :=
-uniform_space.of_core
-{ uniformity := (⨅ ε>0, 𝓟 {p:α×α | edist p.1 p.2 < ε}),
-  refl       := le_infi $ assume ε, le_infi $
-    by simp [set.subset_def, id_rel, edist_self, (>)] {contextual := tt},
-  comp       :=
-    le_infi $ assume ε, le_infi $ assume h,
-    have (2 : ℝ≥0∞) = (2 : ℕ) := by simp,
-    have A : 0 < ε / 2 := ennreal.div_pos_iff.2
-      ⟨ne_of_gt h, by { convert ennreal.nat_ne_top 2 }⟩,
-    lift'_le
-    (mem_infi_of_mem (ε / 2) $ mem_infi_of_mem A (subset.refl _)) $
-    have ∀ (a b c : α), edist a c < ε / 2 → edist c b < ε / 2 → edist a b < ε,
-      from assume a b c hac hcb,
-      calc edist a b ≤ edist a c + edist c b : edist_triangle _ _ _
-        ... < ε / 2 + ε / 2 : ennreal.add_lt_add hac hcb
-        ... = ε : by rw [ennreal.add_halves],
-    by simpa [comp_rel],
-  symm       := tendsto_infi.2 $ assume ε, tendsto_infi.2 $ assume h,
-    tendsto_infi' ε $ tendsto_infi' h $ tendsto_principal_principal.2 $ by simp [edist_comm] }
+uniform_space.of_fun edist edist_self edist_comm edist_triangle $
+  λ ε ε0, ⟨ε / 2, ennreal.half_pos ε0.lt.ne', λ _ h₁ _ h₂,
+      (ennreal.add_lt_add h₁ h₂).trans_eq (ennreal.add_halves _)⟩
 
 -- the uniform structure is embedded in the emetric space structure
 -- to avoid instance diamond issues. See Note [forgetful inheritance].
@@ -175,13 +154,13 @@ theorem uniformity_pseudoedist :
   𝓤 α = ⨅ ε>0, 𝓟 {p:α×α | edist p.1 p.2 < ε} :=
 pseudo_emetric_space.uniformity_edist
 
+theorem uniform_space_edist : ‹pseudo_emetric_space α›.to_uniform_space =
+  uniform_space_of_edist edist edist_self edist_comm edist_triangle :=
+uniform_space_eq uniformity_pseudoedist
+
 theorem uniformity_basis_edist :
   (𝓤 α).has_basis (λ ε : ℝ≥0∞, 0 < ε) (λ ε, {p:α×α | edist p.1 p.2 < ε}) :=
-(@uniformity_pseudoedist α _).symm ▸ has_basis_binfi_principal
-  (λ r hr p hp, ⟨min r p, lt_min hr hp,
-    λ x hx, lt_of_lt_of_le hx (min_le_left _ _),
-    λ x hx, lt_of_lt_of_le hx (min_le_right _ _)⟩)
-  ⟨1, zero_lt_one⟩
+(@uniform_space_edist α _).symm ▸ uniform_space.has_basis_of_fun ⟨1, one_pos⟩ _ _ _ _ _
 
 /-- Characterization of the elements of the uniformity in terms of the extended distance -/
 theorem mem_uniformity_edist {s : set (α×α)} :
@@ -394,16 +373,7 @@ def pseudo_emetric_space.induced {α β} (f : α → β)
   edist_comm          := λ x y, edist_comm _ _,
   edist_triangle      := λ x y z, edist_triangle _ _ _,
   to_uniform_space    := uniform_space.comap f m.to_uniform_space,
-  uniformity_edist    := begin
-    apply @uniformity_dist_of_mem_uniformity _ _ _ _ _ (λ x y, edist (f x) (f y)),
-    refine λ s, mem_comap.trans _,
-    split; intro H,
-    { rcases H with ⟨r, ru, rs⟩,
-      rcases mem_uniformity_edist.1 ru with ⟨ε, ε0, hε⟩,
-      refine ⟨ε, ε0, λ a b h, rs (hε _)⟩, exact h },
-    { rcases H with ⟨ε, ε0, hε⟩,
-      exact ⟨_, edist_mem_uniformity ε0, λ ⟨a, b⟩, hε⟩ }
-  end }
+  uniformity_edist    := (uniformity_basis_edist.comap _).eq_binfi }
 
 /-- Pseudoemetric space instance on subsets of pseudoemetric spaces -/
 instance {α : Type*} {p : α → Prop} [pseudo_emetric_space α] : pseudo_emetric_space (subtype p) :=
@@ -978,16 +948,7 @@ def emetric_space.induced {γ β} (f : γ → β) (hf : function.injective f)
   edist_comm          := λ x y, edist_comm _ _,
   edist_triangle      := λ x y z, edist_triangle _ _ _,
   to_uniform_space    := uniform_space.comap f m.to_uniform_space,
-  uniformity_edist    := begin
-    apply @uniformity_dist_of_mem_uniformity _ _ _ _ _ (λ x y, edist (f x) (f y)),
-    refine λ s, mem_comap.trans _,
-    split; intro H,
-    { rcases H with ⟨r, ru, rs⟩,
-      rcases mem_uniformity_edist.1 ru with ⟨ε, ε0, hε⟩,
-      refine ⟨ε, ε0, λ a b h, rs (hε _)⟩, exact h },
-    { rcases H with ⟨ε, ε0, hε⟩,
-      exact ⟨_, edist_mem_uniformity ε0, λ ⟨a, b⟩, hε⟩ }
-  end }
+  uniformity_edist    := (uniformity_basis_edist.comap _).eq_binfi }
 
 /-- Emetric space instance on subsets of emetric spaces -/
 instance {α : Type*} {p : α → Prop} [emetric_space α] : emetric_space (subtype p) :=

src/topology/metric_space/gluing.lean

@@ -464,7 +464,7 @@ their respective basepoints, plus the distance 1 between the basepoints.
 Since there is an arbitrary choice in this construction, it is not an instance by default. -/
 protected def metric_space : metric_space (Σ i, E i) :=
 begin
-  refine metric_space.of_metrizable sigma.dist _ _ sigma.dist_triangle
+  refine metric_space.of_dist_topology sigma.dist _ _ sigma.dist_triangle
     sigma.is_open_iff _,
   { rintros ⟨i, x⟩, simp [sigma.dist] },
   { rintros ⟨i, x⟩ ⟨j, y⟩,

src/topology/metric_space/pi_nat.lean

@@ -357,7 +357,7 @@ but it does not take care of a possible uniformity. If the `E n` have a uniform
 there will be two non-defeq uniform structures on `Π n, E n`, the product one and the one coming
 from the metric structure. In this case, use `metric_space_of_discrete_uniformity` instead. -/
 protected def metric_space : metric_space (Π n, E n) :=
-metric_space.of_metrizable dist pi_nat.dist_self pi_nat.dist_comm pi_nat.dist_triangle
+metric_space.of_dist_topology dist pi_nat.dist_self pi_nat.dist_comm pi_nat.dist_triangle
   is_open_iff_dist pi_nat.eq_of_dist_eq_zero
 
 /-- Metric space structure on `Π (n : ℕ), E n` when the spaces `E n` have the discrete uniformity,

src/topology/uniform_space/absolute_value.lean

@@ -33,46 +33,21 @@ absolute value, uniform spaces
 -/
 
 open set function filter uniform_space
-open_locale filter
+open_locale filter topology
 
-namespace is_absolute_value
-variables {𝕜 : Type*} [linear_ordered_field 𝕜]
-variables {R : Type*} [comm_ring R] (abv : R → 𝕜) [is_absolute_value abv]
+namespace absolute_value
 
-/-- The uniformity coming from an absolute value. -/
-def uniform_space_core : uniform_space.core R :=
-{ uniformity := (⨅ ε>0, 𝓟 {p:R×R | abv (p.2 - p.1) < ε}),
-  refl := le_infi $ assume ε, le_infi $ assume ε_pos, principal_mono.2
-    (λ ⟨x, y⟩ h, by simpa [show x = y, from h, abv_zero abv]),
-  symm := tendsto_infi.2 $ assume ε, tendsto_infi.2 $ assume h,
-    tendsto_infi' ε $ tendsto_infi' h $ tendsto_principal_principal.2 $ λ ⟨x, y⟩ h,
-      have h : abv (y - x) < ε, by simpa [-sub_eq_add_neg] using h,
-      by rwa abv_sub abv at h,
-  comp := le_infi $ assume ε, le_infi $ assume h, lift'_le
-    (mem_infi_of_mem (ε / 2) $ mem_infi_of_mem (div_pos h zero_lt_two) (subset.refl _)) $
-    have ∀ (a b c : R), abv (c-a) < ε / 2 → abv (b-c) < ε / 2 → abv (b-a) < ε,
-      from assume a b c hac hcb,
-       calc abv (b - a) ≤ _ : abv_sub_le abv b c a
-        ... = abv (c - a) + abv (b - c) : add_comm _ _
-        ... < ε / 2 + ε / 2 : add_lt_add hac hcb
-        ... = ε : by rw [div_add_div_same, add_self_div_two],
-    by simpa [comp_rel] }
+variables {𝕜 : Type*} [linear_ordered_field 𝕜]
+variables {R : Type*} [comm_ring R] (abv : absolute_value R 𝕜)
 
-/-- The uniform structure coming from an absolute value. -/
-def uniform_space : uniform_space R :=
-uniform_space.of_core (uniform_space_core abv)
+/-- The uniform space structure coming from an absolute value. -/
+protected def uniform_space : uniform_space R :=
+uniform_space.of_fun (λ x y, abv (y - x)) (by simp) (λ x y, abv.map_sub y x)
+  (λ x y z, (abv.sub_le _ _ _).trans_eq (add_comm _ _)) $
+  λ ε ε0, ⟨ε / 2, half_pos ε0, λ _ h₁ _ h₂, (add_lt_add h₁ h₂).trans_eq (add_halves ε)⟩
 
-theorem mem_uniformity {s : set (R×R)} :
-  s ∈ (uniform_space_core abv).uniformity ↔
-  (∃ε>0, ∀{a b:R}, abv (b - a) < ε → (a, b) ∈ s) :=
-begin
-  suffices : s ∈ (⨅ ε: {ε : 𝕜 // ε > 0}, 𝓟 {p:R×R | abv (p.2 - p.1) < ε.val}) ↔ _,
-  { rw infi_subtype at this,
-    exact this },
-  rw mem_infi_of_directed,
-  { simp [subset_def] },
-  { rintros ⟨r, hr⟩ ⟨p, hp⟩,
-    exact ⟨⟨min r p, lt_min hr hp⟩, by simp [lt_min_iff, (≥)] {contextual := tt}⟩, },
-end
+theorem has_basis_uniformity :
+  𝓤[abv.uniform_space].has_basis (λ ε : 𝕜, 0 < ε) (λ ε, {p : R × R | abv (p.2 - p.1) < ε}) :=
+uniform_space.has_basis_of_fun (exists_gt _) _ _ _ _ _
 
-end is_absolute_value
+end absolute_value