no goals
α : Type u
β : Type v
γ : Type ?u.531581
δ : Type ?u.531584
ε : Type ?u.531587
ζ : Type ?u.531590
ι : Type u_1
κ : Type ?u.531596
σ : ι → Type u_2
τ : κ → Type ?u.531606
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f : Sigma σ → α
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap fun a => f { fst := i, snd := a }
simp only [isOpenMap_iff_nhds_le, Sigma.forall, Sigma.nhds_eq, map_map, comp]