Theorem: extendedChart_image_nhds_on (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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : M
n : Set M
hn : n ∈ 𝓝 x
hn₂ : n ⊆ e.source
⊢ ↑I ∘ ↑e '' n ∈ 𝓝 (↑(e.extend I) x)
Tactic:
rw [image_comp]
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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : M
n : Set M
hn : n ∈ 𝓝 x
hn₂ : n ⊆ e.source
⊢ ↑I '' (↑e '' n) ∈ 𝓝 (↑(e.extend I) x)

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
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
x : M
n : Set M
hn : n ∈ 𝓝 x
hn₂ : n ⊆ e.source
⊢ ↑I '' (↑e '' n) ∈ 𝓝 (↑(e.extend I) x)
Tactic:
apply I.toOpenEmbedding.isOpenMap.image_mem_nhds (e.image_mem_nhds (hn₂ (mem_of_mem_nhds hn)) hn)
State after:
no goals