α : Type u
β : Type v
γ : Type ?u.528783
δ : Type ?u.528786
ε : Type ?u.528789
ζ : Type ?u.528792
ι : Type u_1
κ : Type ?u.528798
σ : ι → Type u_2
τ : κ → Type ?u.528808
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ Continuous f ↔ ∀ (i : ι), Continuous fun a => f { fst := i, snd := a }
α : Type u
β : Type v
γ : Type ?u.528783
δ : Type ?u.528786
ε : Type ?u.528789
ζ : Type ?u.528792
ι : Type u_1
κ : Type ?u.528798
σ : ι → Type u_2
τ : κ → Type ?u.528808
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ Continuous f ↔ ∀ (i : ι), Continuous fun a => f { fst := i, snd := a }
delta instTopologicalSpaceSigma
α : Type u
β : Type v
γ : Type ?u.528783
δ : Type ?u.528786
ε : Type ?u.528789
ζ : Type ?u.528792
ι : Type u_1
κ : Type ?u.528798
σ : ι → Type u_2
τ : κ → Type ?u.528808
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ (∀ (i : ι), Continuous f) ↔ ∀ (i : ι), Continuous fun a => f { fst := i, snd := a }
α : Type u
β : Type v
γ : Type ?u.528783
δ : Type ?u.528786
ε : Type ?u.528789
ζ : Type ?u.528792
ι : Type u_1
κ : Type ?u.528798
σ : ι → Type u_2
τ : κ → Type ?u.528808
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ Continuous f ↔ ∀ (i : ι), Continuous fun a => f { fst := i, snd := a }
rw [continuous_iSup_dom]
no goals
α : Type u
β : Type v
γ : Type ?u.528783
δ : Type ?u.528786
ε : Type ?u.528789
ζ : Type ?u.528792
ι : Type u_1
κ : Type ?u.528798
σ : ι → Type u_2
τ : κ → Type ?u.528808
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ (∀ (i : ι), Continuous f) ↔ ∀ (i : ι), Continuous fun a => f { fst := i, snd := a }
exact forall_congr' fun _ => continuous_coinduced_dom