no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.68219
inst✝ : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → Set.Nonempty (ball x V ∩ s)
simp [mem_closure_iff_nhds_basis' (nhds_basis_uniformity' (𝓤 α).basis_sets)]