no goals
α : Type u
β : Type v
γ : Type ?u.193723
δ : Type ?u.193726
ε : Type ?u.193729
ζ : Type ?u.193732
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.193743
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
⊢ Continuous f ↔ ∀ (i : ι), Continuous fun a => f a i
simp only [continuous_iInf_rng, continuous_induced_rng, comp]