diff --git a/Mathlib/Topology/UniformSpace/AbsoluteValue.lean b/Mathlib/Topology/UniformSpace/AbsoluteValue.lean index 8cf0f008913f6..c5d7d96fb5ead 100644 --- a/Mathlib/Topology/UniformSpace/AbsoluteValue.lean +++ b/Mathlib/Topology/UniformSpace/AbsoluteValue.lean @@ -25,7 +25,7 @@ follows exactly the same path. absolute value, uniform spaces -/ -open Set Function Filter Topology +open Set Function Filter Uniformity namespace AbsoluteValue diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index 56e32f6c324d8..a101178fc020b 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -358,7 +358,7 @@ def uniformity (α : Type u) [UniformSpace α] : Filter (α × α) := #align uniformity uniformity /-- Notation for the uniformity filter with respect to a non-standard `UniformSpace` instance. -/ -scoped[Topology] notation "𝓤[" u "]" => @uniformity _ u +scoped[Uniformity] notation "𝓤[" u "]" => @uniformity _ u @[ext] theorem uniformSpace_eq : ∀ {u₁ u₂ : UniformSpace α}, 𝓤[u₁] = 𝓤[u₂] → u₁ = u₂ @@ -1092,7 +1092,7 @@ def UniformContinuous [UniformSpace β] (f : α → β) := #align uniform_continuous UniformContinuous /-- Notation for uniform continuity with respect to non-standard `UniformSpace` instances. -/ -scoped[Topology] notation "UniformContinuous[" u₁ ", " u₂ "]" => @UniformContinuous _ _ u₁ u₂ +scoped[Uniformity] notation "UniformContinuous[" u₁ ", " u₂ "]" => @UniformContinuous _ _ u₁ u₂ /-- A function `f : α → β` is *uniformly continuous* on `s : Set α` if `(f x, f y)` tends to the diagonal as `(x, y)` tends to the diagonal while remaining in `s ×ˢ s`.