no goals
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.143123
ε : Type ?u.143126
ζ : Type ?u.143129
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α ⊕ β → γ
⊢ IsOpenMap f ↔ (IsOpenMap fun a => f (inl a)) ∧ IsOpenMap fun b => f (inr b)
simp only [isOpenMap_iff_nhds_le, Sum.forall, nhds_inl, nhds_inr, Filter.map_map, comp]