case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2539023
E : Type u_3
Eₗ : Type ?u.2539029
F : Type u_4
Fₗ : Type ?u.2539035
G : Type ?u.2539038
Gₗ : Type ?u.2539041
𝓕 : Type ?u.2539044
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
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖
x : E
hx : x = 0
⊢ ‖↑f x‖ ≤ C * ‖x‖

case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2539023
E : Type u_3
Eₗ : Type ?u.2539029
F : Type u_4
Fₗ : Type ?u.2539035
G : Type ?u.2539038
Gₗ : Type ?u.2539041
𝓕 : Type ?u.2539044
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
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖
x : E
hx : ¬x = 0
⊢ ‖↑f x‖ ≤ C * ‖x‖
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2539023
E : Type u_3
Eₗ : Type ?u.2539029
F : Type u_4
Fₗ : Type ?u.2539035
G : Type ?u.2539038
Gₗ : Type ?u.2539041
𝓕 : Type ?u.2539044
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
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖
x : E
⊢ ‖↑f x‖ ≤ C * ‖x‖
by_cases hx : x = 0
no goals
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2539023
E : Type u_3
Eₗ : Type ?u.2539029
F : Type u_4
Fₗ : Type ?u.2539035
G : Type ?u.2539038
Gₗ : Type ?u.2539041
𝓕 : Type ?u.2539044
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
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖
x : E
hx : ¬x = 0
⊢ ‖↑f x‖ ≤ C * ‖x‖
exact
  SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf (ne_of_lt (norm_pos_iff.2 hx)).symm
no goals
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2539023
E : Type u_3
Eₗ : Type ?u.2539029
F : Type u_4
Fₗ : Type ?u.2539035
G : Type ?u.2539038
Gₗ : Type ?u.2539041
𝓕 : Type ?u.2539044
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
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖↑f x‖ ≤ C * ‖x‖
x : E
hx : x = 0
⊢ ‖↑f x‖ ≤ C * ‖x‖
simp [hx]