α : Type ?u.24677
V : Type u_1
P : Type u_2
W : Type ?u.24686
Q : Type ?u.24689
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖
α : Type ?u.24677
V : Type u_1
P : Type u_2
W : Type ?u.24686
Q : Type ?u.24689
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
p₁ p₂ p₃ p₄ : P
⊢ dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄
rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V]
no goals
α : Type ?u.24677
V : Type u_1
P : Type u_2
W : Type ?u.24686
Q : Type ?u.24689
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖
exact norm_sub_le _ _