no goals
V : Type ?u.236326
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.236335
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : ℝ≥0
hf : LipschitzWith K ↑f
x : V₁
⊢ ‖↑f x‖ ≤ ↑K * ‖x‖
simpa only [dist_zero_right, map_zero] using hf.dist_le_mul x 0