no goals
α : Type u
β : Type v
γ : Type ?u.529521
δ : Type ?u.529524
ε : Type ?u.529527
ζ : Type ?u.529530
ι : Type u_2
κ : Type u_4
σ : ι → Type u_1
τ : κ → Type u_3
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
⊢ (∀ (i : ι), Continuous fun a => Sigma.map f₁ f₂ { fst := i, snd := a }) ↔ ∀ (i : ι), Continuous (f₂ i)
simp only [Sigma.map, embedding_sigmaMk.continuous_iff, comp]