no goals
α✝ : Type ?u.154580
β : Type ?u.154583
γ : Type ?u.154586
δ : Type ?u.154589
inst✝¹ : TopologicalSpace α✝
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ NeBot (𝓝[Set.pi I s] x) ↔ ∀ (i : ι), i ∈ I → NeBot (𝓝[s i] x i)
simp [neBot_iff, nhdsWithin_pi_eq_bot]