---

Step * of Lemma rv-norm-triangle-inequality2

∀[rv:InnerProductSpace]. ∀[x,y,z:Point].  (||x - z|| ≤ (||x - y|| + ||y - z||))
BY
{ (Auto THEN (RWO "rv-norm-triangle-inequality<" 0 THENA Auto)) }

1
1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. z : Point
⊢ ||x - z|| ≤ ||x - y + y - z||

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[x,y,z:Point].    (||x  -  z||  \mleq{}  (||x  -  y||  +  ||y  -  z||))


By

---

Latex:
(Auto  THEN  (RWO  "rv-norm-triangle-inequality<"  0  THENA  Auto))

---

Home Index