no goals
X : Type ?u.16376
Y : Type ?u.16379
Z : Type ?u.16382
α : Type ?u.16385
ι : Type u_1
π : ι → Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f✝ : X → Y
f g : (i : ι) → π i
⊢ f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i
simp only [Specializes, nhds_pi, pi_le_pi]