V : Type ?u.232658
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.232667
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ ‖↑f (x - y)‖ ≤ ↑{ val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } * ‖x - y‖
V : Type ?u.232658
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.232667
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ dist (↑f x) (↑f y) ≤ ↑{ val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } * dist x y
rw [dist_eq_norm, dist_eq_norm, ← map_sub]
no goals
V : Type ?u.232658
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.232667
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ ‖↑f (x - y)‖ ≤ ↑{ val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } * ‖x - y‖
apply le_opNorm