no goals
α : Type u
β : Type v
γ : Type ?u.119697
δ : Type ?u.119700
ε : Type ?u.119703
ζ : Type ?u.119706
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
u : Set α
hu : IsOpen u
⊢ IsOpen (inl '' u)
simpa [isOpen_sum_iff, preimage_image_eq u Sum.inl_injective]