α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.72743
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
⊢ IsOpenMap (f ∘ ↑h) → IsOpenMap f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.72743
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
⊢ IsOpenMap (f ∘ ↑h) ↔ IsOpenMap f
refine' ⟨_, fun hf => hf.comp h.isOpenMap⟩
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.72743
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
hf : IsOpenMap (f ∘ ↑h)
⊢ IsOpenMap f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.72743
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
⊢ IsOpenMap (f ∘ ↑h) → IsOpenMap f
intro hf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.72743
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
hf : IsOpenMap (f ∘ ↑h)
⊢ IsOpenMap ((f ∘ ↑h) ∘ ↑(Homeomorph.symm h))
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.72743
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
hf : IsOpenMap (f ∘ ↑h)
⊢ IsOpenMap f
rw [← Function.comp.right_id f, ← h.self_comp_symm, ← Function.comp.assoc]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.72743
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
hf : IsOpenMap (f ∘ ↑h)
⊢ IsOpenMap ((f ∘ ↑h) ∘ ↑(Homeomorph.symm h))
exact hf.comp h.symm.isOpenMap