no goals
α : Type u
β : Type v
γ : Type ?u.120234
δ : Type ?u.120237
ε : Type ?u.120240
ζ : Type ?u.120243
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
u : Set β
hu : IsOpen u
⊢ IsOpen (inr '' u)
simpa [isOpen_sum_iff, preimage_image_eq u Sum.inr_injective]