𝕜 : 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.30683
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E × F
⊢ ‖↑(LinearMap.snd 𝕜 E F) x‖ ≤ 1 * ‖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.30683
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
⊢ IsBoundedLinearMap 𝕜 fun x => x.snd
refine' (LinearMap.snd 𝕜 E F).isLinear.with_bound 1 fun 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.30683
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E × F
⊢ ‖↑(LinearMap.snd 𝕜 E F) x‖ ≤ ‖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.30683
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E × F
⊢ ‖↑(LinearMap.snd 𝕜 E F) x‖ ≤ 1 * ‖x‖
rw [one_mul]
no goals
𝕜 : 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.30683
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E × F
⊢ ‖↑(LinearMap.snd 𝕜 E F) x‖ ≤ ‖x‖
exact le_max_right _ _