Theorem: PartialHomeomorph.isOpenMapOn_source (Sard/ManifoldAux.lean)

State before:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : Set M
hopen : IsOpen s
hs : s ⊆ e.source
⊢ IsOpen (↑e '' s)
Tactic:
rw [(image_eq_target_inter_inv_preimage (e := e) hs)]
State after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : Set M
hopen : IsOpen s
hs : s ⊆ e.source
⊢ IsOpen (e.target ∩ ↑e.symm ⁻¹' s)

State before:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : Set M
hopen : IsOpen s
hs : s ⊆ e.source
⊢ IsOpen (e.target ∩ ↑e.symm ⁻¹' s)
Tactic:
exact e.continuousOn_invFun.isOpen_inter_preimage e.open_target hopen
State after:
no goals