no goals
α : Type u
β : Type v
γ : Type ?u.312479
δ : Type ?u.312482
ε : Type ?u.312485
ζ : Type ?u.312488
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.312499
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (π i)
a : (i : ι) → π i
⊢ Set.pi I s ∈ 𝓝 a ↔ ∀ (i : ι), i ∈ I → s i ∈ 𝓝 (a i)
rw [nhds_pi, pi_mem_pi_iff hI]