diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean index f828a823ee8cd..4eae4a2c7b4eb 100644 --- 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 <| α → β