𝕜 : Type u_2
𝕜₂ : Type ?u.2599087
𝕜₃ : Type ?u.2599090
E : Type u_1
Eₗ : Type ?u.2599096
F : Type ?u.2599099
Fₗ : Type ?u.2599102
G : Type ?u.2599105
Gₗ : Type ?u.2599108
𝓕 : Type ?u.2599111
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✝ : Nontrivial E
⊢ ∃ x, ‖x‖ ≠ 0
𝕜 : Type u_2
𝕜₂ : Type ?u.2599087
𝕜₃ : Type ?u.2599090
E : Type u_1
Eₗ : Type ?u.2599096
F : Type ?u.2599099
Fₗ : Type ?u.2599102
G : Type ?u.2599105
Gₗ : Type ?u.2599108
𝓕 : Type ?u.2599111
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✝ : Nontrivial E
⊢ ‖id 𝕜 E‖ = 1
refine' norm_id_of_nontrivial_seminorm _
case intro
𝕜 : Type u_2
𝕜₂ : Type ?u.2599087
𝕜₃ : Type ?u.2599090
E : Type u_1
Eₗ : Type ?u.2599096
F : Type ?u.2599099
Fₗ : Type ?u.2599102
G : Type ?u.2599105
Gₗ : Type ?u.2599108
𝓕 : Type ?u.2599111
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✝ : Nontrivial E
x : E
hx : x ≠ 0
⊢ ∃ x, ‖x‖ ≠ 0
𝕜 : Type u_2
𝕜₂ : Type ?u.2599087
𝕜₃ : Type ?u.2599090
E : Type u_1
Eₗ : Type ?u.2599096
F : Type ?u.2599099
Fₗ : Type ?u.2599102
G : Type ?u.2599105
Gₗ : Type ?u.2599108
𝓕 : Type ?u.2599111
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✝ : Nontrivial E
⊢ ∃ x, ‖x‖ ≠ 0
obtain ⟨x, hx⟩ := exists_ne (0 : E)
no goals
case intro
𝕜 : Type u_2
𝕜₂ : Type ?u.2599087
𝕜₃ : Type ?u.2599090
E : Type u_1
Eₗ : Type ?u.2599096
F : Type ?u.2599099
Fₗ : Type ?u.2599102
G : Type ?u.2599105
Gₗ : Type ?u.2599108
𝓕 : Type ?u.2599111
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✝ : Nontrivial E
x : E
hx : x ≠ 0
⊢ ∃ x, ‖x‖ ≠ 0
exact ⟨x, ne_of_gt (norm_pos_iff.2 hx)⟩