---

Step * of Lemma real-vec-triangle-inequality

∀[n:ℕ]. ∀[x,y,z:ℝ^n].  (d(x;z) ≤ (d(x;y) + d(y;z)))
BY
{ (Auto THEN Unfold `real-vec-dist` 0 THEN (RWO "Minkowski-inequality1<" 0⋅ THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. z : ℝ^n
⊢ ||x - z|| ≤ ||x - y + y - z||

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y,z:\mBbbR{}\^{}n].    (d(x;z)  \mleq{}  (d(x;y)  +  d(y;z)))


By

---

Latex:
(Auto  THEN  Unfold  `real-vec-dist`  0  THEN  (RWO  "Minkowski-inequality1<"  0\mcdot{}  THENA  Auto))

---

Home Index