case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
U : ι → Set (α × α)
h : HasBasis (𝓤 α) p U
s : Set α
x : α
⊢ (x ∈ ⋂ (i : ι) (_ : p i), ⋃ (x : α) (_ : x ∈ s), ball x (U i)) ↔ x ∈ closure s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
U : ι → Set (α × α)
h : HasBasis (𝓤 α) p U
s : Set α
⊢ (⋂ (i : ι) (_ : p i), ⋃ (x : α) (_ : x ∈ s), ball x (U i)) = closure s
ext x
no goals
case h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
U : ι → Set (α × α)
h : HasBasis (𝓤 α) p U
s : Set α
x : α
⊢ (x ∈ ⋂ (i : ι) (_ : p i), ⋃ (x : α) (_ : x ∈ s), ball x (U i)) ↔ x ∈ closure s
simp [mem_closure_iff_nhds_basis (nhds_basis_uniformity h), ball]