α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.139304
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ : α → β
g : β → γ
f : α → β
hg : IsOpenMap g
hf : IsOpenMap f
s : Set α
hs : IsOpen s
⊢ IsOpen (g '' (f '' s))
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.139304
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ : α → β
g : β → γ
f : α → β
hg : IsOpenMap g
hf : IsOpenMap f
s : Set α
hs : IsOpen s
⊢ IsOpen (g ∘ f '' s)
rw [image_comp]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.139304
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ : α → β
g : β → γ
f : α → β
hg : IsOpenMap g
hf : IsOpenMap f
s : Set α
hs : IsOpen s
⊢ IsOpen (g '' (f '' s))
exact hg _ (hf _ hs)