α : Type u_1
β : Type u_2
γ : Type ?u.49930
δ : Type ?u.49933
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
this : ↑e '' s = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s
⊢ IsOpen (↑e '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.49930
δ : Type ?u.49933
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
⊢ IsOpen (↑e '' s)
have : e '' s = e.target ∩ e.symm ⁻¹' s := e.toLocalEquiv.image_eq_target_inter_inv_preimage h
α : Type u_1
β : Type u_2
γ : Type ?u.49930
δ : Type ?u.49933
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
this : ↑e '' s = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s
⊢ IsOpen (e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s)
α : Type u_1
β : Type u_2
γ : Type ?u.49930
δ : Type ?u.49933
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
this : ↑e '' s = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s
⊢ IsOpen (↑e '' s)
rw [this]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.49930
δ : Type ?u.49933
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
this : ↑e '' s = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s
⊢ IsOpen (e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s)
exact e.continuousOn_symm.preimage_open_of_open e.open_target hs