no goals
𝕜 : Type u_3
R : Type ?u.116219
V : Type u_2
W : Type u_1
W₂ : Type ?u.116228
P : Type ?u.116231
Q : Type ?u.116234
Q₂ : Type ?u.116237
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
h : ↑f 0 = 0
⊢ ‖f‖ = max ‖↑f 0‖ ‖contLinear f‖
rw [norm_def]
no goals
𝕜 : Type u_3
R : Type ?u.116219
V : Type u_2
W : Type u_1
W₂ : Type ?u.116228
P : Type ?u.116231
Q : Type ?u.116234
Q₂ : Type ?u.116237
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
h : ↑f 0 = 0
⊢ max ‖↑f 0‖ ‖contLinear f‖ = max 0 ‖contLinear f‖
rw [h, norm_zero]