case intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ
ε0 : 0 < ε
hε : ↑f ⁻¹' ball 0 ε ⊆ ball 0 1
⊢ ∃ K, AntilipschitzWith K ↑f
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
⊢ ∃ K, AntilipschitzWith K ↑f
rcases ((nhds_basis_ball.comap _).le_basis_iff nhds_basis_ball).1 hf 1 one_pos with ⟨ε, ε0, hε⟩
case intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ
ε0 : 0 < ε
hε : ∀ (x : E), ‖↑f x‖ < ε → ‖x‖ < 1
⊢ ∃ K, AntilipschitzWith K ↑f
case intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ
ε0 : 0 < ε
hε : ↑f ⁻¹' ball 0 ε ⊆ ball 0 1
⊢ ∃ K, AntilipschitzWith K ↑f
simp only [Set.subset_def, Set.mem_preimage, mem_ball_zero_iff] at hε
case intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
⊢ ∃ K, AntilipschitzWith K ↑f
case intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ
ε0 : 0 < ε
hε : ∀ (x : E), ‖↑f x‖ < ε → ‖x‖ < 1
⊢ ∃ K, AntilipschitzWith K ↑f
lift ε to ℝ≥0 using ε0.le
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ K, AntilipschitzWith K ↑f
case intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
⊢ ∃ K, AntilipschitzWith K ↑f
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ K, AntilipschitzWith K ↑f
refine' ⟨ε⁻¹ * ‖c‖₊, AddMonoidHomClass.antilipschitz_of_bound f fun x => _⟩
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ↑f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖

case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ¬↑f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
by_cases hx : f x = 0
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ¬↑f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
have hc₀ : c ≠ 0 := norm_pos_iff.1 (one_pos.trans hc)
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖↑σ₁₂ c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
rw [← h.1] at hc
case neg.intro.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖↑σ₁₂ c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖↑σ₁₂ c ^ n • ↑f x‖ < ↑ε
hle : ‖↑σ₁₂ c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖↑σ₁₂ c‖ * ‖↑f x‖
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖↑σ₁₂ c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
rcases rescale_to_shell_zpow hc ε0 hx with ⟨n, -, hlt, -, hle⟩
case neg.intro.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖↑σ₁₂ c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖↑f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖↑f x‖
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
case neg.intro.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖↑σ₁₂ c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖↑σ₁₂ c ^ n • ↑f x‖ < ↑ε
hle : ‖↑σ₁₂ c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖↑σ₁₂ c‖ * ‖↑f x‖
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
simp only [← map_zpow₀, h.1, ← map_smulₛₗ] at hlt hle
no goals
case neg.intro.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖↑σ₁₂ c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖↑f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖↑f x‖
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
calc
  ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ := by
    rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
  _ ≤ ‖c ^ n‖⁻¹ * 1 := (mul_le_mul_of_nonneg_left (hε _ hlt).le (inv_nonneg.2 (norm_nonneg _)))
  _ ≤ ε⁻¹ * ‖c‖ * ‖f x‖ := by rwa [mul_one]
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hf : Filter.comap (↑f) (𝓝 (↑f x)) ≤ 𝓝 0
hx : ↑f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ↑f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
rw [← hx] at hf
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
hf : Filter.comap (↑f) (𝓝 (↑f 0)) ≤ 𝓝 0
hx : ↑f 0 = 0
⊢ ‖0‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f 0‖
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hf : Filter.comap (↑f) (𝓝 (↑f x)) ≤ 𝓝 0
hx : ↑f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f x‖
obtain rfl : x = 0 := Specializes.eq (specializes_iff_pure.2 <|
  ((Filter.tendsto_pure_pure _ _).mono_right (pure_le_nhds _)).le_comap.trans hf)
no goals
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
hf : Filter.comap (↑f) (𝓝 (↑f 0)) ≤ 𝓝 0
hx : ↑f 0 = 0
⊢ ‖0‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖↑f 0‖
exact norm_zero.trans_le (mul_nonneg (NNReal.coe_nonneg _) (norm_nonneg _))
no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖↑σ₁₂ c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖↑f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖↑f x‖
⊢ ‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖
rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2566867
E : Type u_3
Eₗ : Type ?u.2566873
F : Type u_4
Fₗ : Type ?u.2566879
G : Type ?u.2566882
Gₗ : Type ?u.2566885
𝓕 : Type ?u.2566888
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
inst✝ : NormedSpace 𝕜 Fₗ
c✝ : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f✝ g : E →SL[σ₁₂] F
x✝ y z : E
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (↑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖↑f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖↑σ₁₂ c‖
x : E
hx : ¬↑f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖↑f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖↑f x‖
⊢ ‖c ^ n‖⁻¹ * 1 ≤ ↑ε⁻¹ * ‖c‖ * ‖↑f x‖
rwa [mul_one]