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