Skip to content

Commit

Permalink
chore: move all UniformSpace-related notations in scope Uniformity (#…
Browse files Browse the repository at this point in the history
  • Loading branch information
ADedecker committed Aug 15, 2023
1 parent 0e5c7d3 commit f3df63e
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion Mathlib/Topology/UniformSpace/AbsoluteValue.lean
Expand Up @@ -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

Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Topology/UniformSpace/Basic.lean
Expand Up @@ -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₂
Expand Down Expand Up @@ -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`.
Expand Down

0 comments on commit f3df63e

Please sign in to comment.