∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] [inst : DecidableEq ι]
  {s : Set ((a : ι) → A a)} {x : (a : ι) → A a}, s ∈ nhds x → ∀ (y : (a : ι) → A a), ∃ I, I.piecewise x y ∈ s