no goals
V : Type ?u.497709
W : Type ?u.497712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.497721
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ : NormedAddGroupHom V W
f : NormedAddGroupHom V₁ V₂
h : NormNoninc (-f)
x : V₁
⊢ ‖↑f x‖ ≤ ‖x‖
simpa using h x