no goals
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.143893
ε : Type ?u.143896
ζ : Type ?u.143899
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → γ
⊢ IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g
simp only [isOpenMap_sum, elim_inl, elim_inr]