α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.59981
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ ∃ V_1, V_1 ∈ 𝓤 α ∧ ball x V_1 ⊆ ball x V
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.59981
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ ball x V ∈ 𝓝 x
rw [UniformSpace.mem_nhds_iff]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.59981
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ ∃ V_1, V_1 ∈ 𝓤 α ∧ ball x V_1 ⊆ ball x V
exact ⟨V, V_in, Subset.rfl⟩