Theorem: PartialHomeomorph.symm_isOpenMapOn_target (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
t : Set H
hopen : IsOpen t
ht : t ⊆ e.target
⊢ IsOpen (e.invFun '' t)
Tactic:
have r : e.invFun '' t = e.source ∩ ↑e ⁻¹' t := symm_image_eq_source_inter_preimage (e := e) ht
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
t : Set H
hopen : IsOpen t
ht : t ⊆ e.target
r : e.invFun '' t = e.source ∩ ↑e ⁻¹' t
⊢ IsOpen (e.invFun '' t)

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
t : Set H
hopen : IsOpen t
ht : t ⊆ e.target
r : e.invFun '' t = e.source ∩ ↑e ⁻¹' t
⊢ IsOpen (e.invFun '' t)
Tactic:
exact r ▸ e.continuousOn_toFun.isOpen_inter_preimage e.open_source hopen
State after:
no goals