case intro.intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.309590
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.309693
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : ContinuousLinearMap.NonlinearRightInverse f'
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen t
xt : x ∈ t
⊢ f '' s ∈ 𝓝 (f x)
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.309590
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.309693
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : ContinuousLinearMap.NonlinearRightInverse f'
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
⊢ f '' s ∈ 𝓝 (f x)
obtain ⟨t, hts, ht, xt⟩ : ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := _root_.mem_nhds_iff.1 hs
case intro.intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.309590
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.309693
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : ContinuousLinearMap.NonlinearRightInverse f'
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen t
xt : x ∈ t
this : f '' t ∈ 𝓝 (f x)
⊢ f '' s ∈ 𝓝 (f x)
case intro.intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.309590
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.309693
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : ContinuousLinearMap.NonlinearRightInverse f'
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen t
xt : x ∈ t
⊢ f '' s ∈ 𝓝 (f x)
have := IsOpen.mem_nhds ((hf.mono_set hts).open_image f'symm ht hc) (mem_image_of_mem _ xt)
no goals
case intro.intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.309590
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.309693
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : ContinuousLinearMap.NonlinearRightInverse f'
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen t
xt : x ∈ t
this : f '' t ∈ 𝓝 (f x)
⊢ f '' s ∈ 𝓝 (f x)
exact mem_of_superset this (image_subset _ hts)