∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] {I : Set ι} {s : (i : ι) → Set (X i)}
  {x : (i : ι) → X i}, nhdsWithin x (I.pi s) = ⊥ ↔ ∃ i ∈ I, nhdsWithin (x i) (s i) = ⊥