[Merged by Bors] - feat: define UniformSpace.ofFun

Mathlib/Algebra/Order/AbsoluteValue.lean

@@ -47,8 +47,6 @@ namespace AbsoluteValue
 -- Porting note: Removing nolints.
 -- attribute [nolint doc_blame] AbsoluteValue.toMulHom
 
--- initialize_simps_projections AbsoluteValue (to_mul_hom_to_fun → apply)
-
 section OrderedSemiring
 
 section Semiring
@@ -86,6 +84,11 @@ theorem ext ⦃f g : AbsoluteValue R S⦄ : (∀ x, f x = g x) → f = g :=
   FunLike.ext _ _
 #align absolute_value.ext AbsoluteValue.ext
 
+/-- See Note [custom simps projection]. -/
+def Simps.apply (f : AbsoluteValue R S) : R → S := f
+
+initialize_simps_projections AbsoluteValue (toMulHom_toFun → apply)
+
 -- Porting note:
 -- These helper instances are unhelpful in Lean 4, so omitting:
 -- /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
@@ -249,7 +252,7 @@ section LinearOrderedRing
 variable {R S : Type _} [Semiring R] [LinearOrderedRing S] (abv : AbsoluteValue R S)
 
 /-- `AbsoluteValue.abs` is `abs` as a bundled `AbsoluteValue`. -/
---@[simps] -- Porting note: Removed simps lemma
+@[simps]
 protected def abs : AbsoluteValue S S where
   toFun := abs
   nonneg' := abs_nonneg
@@ -323,7 +326,7 @@ instance _root_.AbsoluteValue.isAbsoluteValue (abv : AbsoluteValue R S) :
 #align absolute_value.is_absolute_value AbsoluteValue.isAbsoluteValue
 
 /-- Convert an unbundled `IsAbsoluteValue` to a bundled `AbsoluteValue`. -/
---@[simps] -- Porting note: Removed simps lemma
+@[simps]
 def toAbsoluteValue : AbsoluteValue R S where
   toFun := abv
   add_le' := abv_add'

Mathlib/Order/Filter/Basic.lean

@@ -2995,6 +2995,11 @@ theorem tendsto_infᵢ' {f : α → β} {x : ι → Filter α} {y : Filter β} (
   hi.mono_left <| infᵢ_le _ _
 #align filter.tendsto_infi' Filter.tendsto_infᵢ'
 
+theorem tendsto_infᵢ_infᵢ {f : α → β} {x : ι → Filter α} {y : ι → Filter β}
+    (h : ∀ i, Tendsto f (x i) (y i)) : Tendsto f (infᵢ x) (infᵢ y) :=
+  tendsto_infᵢ.2 fun i => tendsto_infᵢ' i (h i)
+#align filter.tendsto_infi_infi Filter.tendsto_infᵢ_infᵢ
+
 @[simp]
 theorem tendsto_sup {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} :
     Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y := by
@@ -3010,6 +3015,11 @@ theorem tendsto_supᵢ {f : α → β} {x : ι → Filter α} {y : Filter β} :
     Tendsto f (⨆ i, x i) y ↔ ∀ i, Tendsto f (x i) y := by simp only [Tendsto, map_supᵢ, supᵢ_le_iff]
 #align filter.tendsto_supr Filter.tendsto_supᵢ
 
+theorem tendsto_supᵢ_supᵢ {f : α → β} {x : ι → Filter α} {y : ι → Filter β}
+    (h : ∀ i, Tendsto f (x i) (y i)) : Tendsto f (supᵢ x) (supᵢ y) :=
+  tendsto_supᵢ.2 fun i => (h i).mono_right <| le_supᵢ _ _
+#align filter.tendsto_supr_supr Filter.tendsto_supᵢ_supᵢ
+
 @[simp] theorem 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]

Mathlib/Topology/UniformSpace/AbsoluteValue.lean

@@ -28,59 +28,23 @@ follows exactly the same path.
 absolute value, uniform spaces
 -/
 
+open Set Function Filter Topology
 
-open Set Function Filter UniformSpace
-
-open Filter
-
-namespace IsAbsoluteValue
+namespace AbsoluteValue
 
 variable {𝕜 : Type _} [LinearOrderedField 𝕜]
-
-variable {R : Type _} [CommRing R] (abv : R → 𝕜) [IsAbsoluteValue abv]
-
-/-- The uniformity coming from an absolute value. -/
-def uniformSpaceCore : UniformSpace.Core R
-    where
-  uniformity := ⨅ ε > 0, 𝓟 { p : R × R | abv (p.2 - p.1) < ε }
-  refl := le_infᵢ fun ε => le_infᵢ fun ε_pos =>
-    principal_mono.2 fun ⟨x, y⟩ h => by have : x = y := (mem_idRel.1 h); simpa [abv_zero, this]
-  symm := tendsto_infᵢ.2 fun ε => tendsto_infᵢ.2 fun h =>
-    tendsto_infᵢ' ε <| tendsto_infᵢ' h <| tendsto_principal_principal.2 fun ⟨x, y⟩ h => by
-      have h : abv (y - x) < ε := by simpa using h
-      rwa [abv_sub abv] at h
-  comp := le_infᵢ fun ε => le_infᵢ fun h => lift'_le (mem_infᵢ_of_mem (ε / 2) <|
-    mem_infᵢ_of_mem (div_pos h zero_lt_two) (Subset.refl _)) <| by
-      have : ∀ a b c : R, abv (c - a) < ε / 2 → abv (b - c) < ε / 2 → abv (b - a) < ε :=
-        fun 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]
-
-      simpa [compRel]
-#align is_absolute_value.uniform_space_core IsAbsoluteValue.uniformSpaceCore
+variable {R : Type _} [CommRing R] (abv : AbsoluteValue R 𝕜)
 
 /-- The uniform structure coming from an absolute value. -/
 def uniformSpace : UniformSpace R :=
-  UniformSpace.ofCore (uniformSpaceCore abv)
-#align is_absolute_value.uniform_space IsAbsoluteValue.uniformSpace
-
--- Porting note: changed `ε > 0` to `0 < ε`
--- Porting note: because lean faied to synthesize `Nonempty { ε // ε > 0 }`, but ok with 0 < ε
+  .ofFun (fun x y => abv (y - x)) (by simp) (fun x y => abv.map_sub y x)
+    (fun x y z => (abv.sub_le _ _ _).trans_eq (add_comm _ _))
+    fun ε ε0 => ⟨ε / 2, half_pos ε0, fun _ h₁ _ h₂ => (add_lt_add h₁ h₂).trans_eq (add_halves ε)⟩
+#align absolute_value.uniform_space AbsoluteValue.uniformSpace
 
-theorem mem_uniformity {s : Set (R × R)} :
-    s ∈ (uniformSpaceCore abv).uniformity ↔ ∃ ε > 0, ∀ {a b : R}, abv (b - a) < ε → (a, b) ∈ s := by
-  suffices (s ∈ ⨅ ε : { ε : 𝕜 // 0 < ε }, 𝓟 { p : R × R | abv (p.2 - p.1) < ε.val }) ↔ _
-    by
-    rw [infᵢ_subtype] at this
-    exact this
-  rw [mem_infᵢ_of_directed]
-  · simp [subset_def]
-  · rintro ⟨r, hr⟩ ⟨p, hp⟩
-    exact
-      ⟨⟨min r p, lt_min hr hp⟩, by simp (config := { contextual := true })⟩
-#align is_absolute_value.mem_uniformity IsAbsoluteValue.mem_uniformity
+theorem hasBasis_uniformity :
+    𝓤[abv.uniformSpace].HasBasis ((0 : 𝕜) < ·) fun ε => { p : R × R | abv (p.2 - p.1) < ε } :=
+  UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _
+#align absolute_value.has_basis_uniformity AbsoluteValue.hasBasis_uniformity
 
-end IsAbsoluteValue
+end AbsoluteValue

Mathlib/Topology/UniformSpace/Basic.lean

@@ -387,6 +387,34 @@ theorem UniformSpace.replaceTopology_eq {α : Type _} [i : TopologicalSpace α]
   u.ofCoreEq_toCore _ _
 #align uniform_space.replace_topology_eq UniformSpace.replaceTopology_eq
 
+-- porting note: rfc: use `UniformSpace.Core.mkOfBasis`? This will change defeq here and there
+/-- Define a `UniformSpace` using a "distance" function. The function can be, e.g., the
+distance in a (usual or extended) metric space or an absolute value on a ring. -/
+def UniformSpace.ofFun {α : Type u} {β : Type v} [OrderedAddCommMonoid β]
+    (d : α → α → β) (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
+    (triangle : ∀ x y z, d x z ≤ d x y + d y z)
+    (half : ∀ ε > (0 : β), ∃ δ > (0 : β), ∀ x < δ, ∀ y < δ, x + y < ε) :
+    UniformSpace α :=
+.ofCore
+  { uniformity := ⨅ r > 0, 𝓟 { x | d x.1 x.2 < r }
+    refl := le_infᵢ₂ fun r hr => principal_mono.2 <| idRel_subset.2 fun x => by simpa [refl]
+    symm := tendsto_infᵢ_infᵢ fun r => tendsto_infᵢ_infᵢ fun _ => tendsto_principal_principal.2
+      fun x hx => by rwa [mem_setOf, symm]
+    comp := le_infᵢ₂ fun r hr => let ⟨δ, h0, hδr⟩ := half r hr; le_principal_iff.2 <|
+      mem_of_superset (mem_lift' <| mem_infᵢ_of_mem δ <| mem_infᵢ_of_mem h0 <| mem_principal_self _)
+        fun (x, z) ⟨y, h₁, h₂⟩ => (triangle _ _ _).trans_lt (hδr _ h₁ _ h₂) }
+#align uniform_space.of_fun UniformSpace.ofFun
+
+theorem UniformSpace.hasBasis_ofFun {α : Type u} {β : Type v} [LinearOrderedAddCommMonoid β]
+    (h₀ : ∃ x : β, 0 < x) (d : α → α → β) (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
+    (triangle : ∀ x y z, d x z ≤ d x y + d y z)
+    (half : ∀ ε > (0 : β), ∃ δ > (0 : β), ∀ x < δ, ∀ y < δ, x + y < ε) :
+    𝓤[.ofFun d refl symm triangle half].HasBasis ((0 : β) < ·) (fun ε => { x | d x.1 x.2 < ε }) :=
+  hasBasis_binfᵢ_principal'
+    (fun ε₁ h₁ ε₂ h₂ => ⟨min ε₁ ε₂, lt_min h₁ h₂, fun _x hx => lt_of_lt_of_le hx (min_le_left _ _),
+      fun _x hx => lt_of_lt_of_le hx (min_le_right _ _)⟩) h₀
+#align uniform_space.has_basis_of_fun UniformSpace.hasBasis_ofFun
+
 section UniformSpace
 
 variable [UniformSpace α]