arguments

leanprover-community · Sep 25, 2024 · f22e9cb · f22e9cb
1 parent 155b53f
commit f22e9cb
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
@@ -157,9 +157,9 @@ open UniformConvergence
 
 variable {α β : Type*} {𝔖 : Set (Set α)}
 
-instance [Nonempty β] : Nonempty (α →ᵤ β) := Pi.instNonempty _
+instance [Nonempty β] : Nonempty (α →ᵤ β) := Pi.instNonempty
 
-instance [Nonempty β] : Nonempty (α →ᵤ[𝔖] β) := Pi.instNonempty _
+instance [Nonempty β] : Nonempty (α →ᵤ[𝔖] β) := Pi.instNonempty
 
 instance [Subsingleton β] : Subsingleton (α →ᵤ β) :=
   inferInstanceAs <| Subsingleton <| α → β