𝕜 : Type u_3
E : Type u_2
M : Type u_1
H : Type u_4
E' : Type ?u.223809
M' : Type ?u.223812
H' : Type ?u.223815
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'
ht : t ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(LocalEquiv.symm (extChartAt I x)) (↑(extChartAt I x) x))
𝕜 : Type u_3
E : Type u_2
M : Type u_1
H : Type u_4
E' : Type ?u.223809
M' : Type ?u.223812
H' : Type ?u.223815
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'
ht : t ∈ 𝓝 x
⊢ ↑(LocalEquiv.symm (extChartAt I x)) ⁻¹' t ∈ 𝓝 (↑(extChartAt I x) x)
apply (continuousAt_extChartAt_symm I x).preimage_mem_nhds
no goals
𝕜 : Type u_3
E : Type u_2
M : Type u_1
H : Type u_4
E' : Type ?u.223809
M' : Type ?u.223812
H' : Type ?u.223815
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'
ht : t ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(LocalEquiv.symm (extChartAt I x)) (↑(extChartAt I x) x))
rwa [(extChartAt I x).left_inv (mem_extChartAt_source _ _)]