α : Type ?u.29026
V : Type u_1
P : Type u_2
W : Type ?u.29035
Q : Type ?u.29038
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
⊢ ↑(nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄)) ≤ ↑(nndist p₁ p₃) + ↑(nndist p₂ p₄)
α : Type ?u.29026
V : Type u_1
P : Type u_2
W : Type ?u.29035
Q : Type ?u.29038
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
⊢ edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄
simp only [edist_nndist]
α : Type ?u.29026
V : Type u_1
P : Type u_2
W : Type ?u.29035
Q : Type ?u.29038
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
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
α : Type ?u.29026
V : Type u_1
P : Type u_2
W : Type ?u.29035
Q : Type ?u.29038
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
⊢ ↑(nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄)) ≤ ↑(nndist p₁ p₃) + ↑(nndist p₂ p₄)
norm_cast
no goals
α : Type ?u.29026
V : Type u_1
P : Type u_2
W : Type ?u.29035
Q : Type ?u.29038
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
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
apply dist_vsub_vsub_le