𝕜 : Type u_4
E : Type u_1
M : Type u_2
H : Type u_3
E' : Type ?u.207999
M' : Type ?u.208002
H' : Type ?u.208005
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s✝ t : Set M
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
s : Set E
hs : IsOpen s
⊢ IsOpen ((extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' s)
𝕜 : Type u_4
E : Type u_1
M : Type u_2
H : Type u_3
E' : Type ?u.207999
M' : Type ?u.208002
H' : Type ?u.208005
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s✝ t : Set M
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
s : Set E
hs : IsOpen s
⊢ IsOpen ((chartAt H x).toLocalEquiv.source ∩ ↑(extChartAt I x) ⁻¹' s)
rw [← extChartAt_source I]
no goals
𝕜 : Type u_4
E : Type u_1
M : Type u_2
H : Type u_3
E' : Type ?u.207999
M' : Type ?u.208002
H' : Type ?u.208005
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s✝ t : Set M
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
s : Set E
hs : IsOpen s
⊢ IsOpen ((extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' s)
exact isOpen_extChartAt_preimage' I x hs