no goals
ι : Sort u_2
α : Type u_1
β : Type ?u.6309
X : Type ?u.6312
Y : Type ?u.6315
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (𝓝 l) p fun i => {l' | s i ∈ l'}
simpa only [Iic_principal] using h.nhds