---

Step * 1 of Lemma rv-norm-triangle-inequality2


1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. z : Point
⊢ ||x - z|| ≤ ||x - y + y - z||
BY
{ (Assert ⌜x - y + y - z ≡ x - z⌝⋅ THENM (RWO  "-1" 0 THEN Auto)) }

1
.....assertion..... 
1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. z : Point
⊢ x - y + y - z ≡ x - z

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  Point
3.  y  :  Point
4.  z  :  Point
\mvdash{}  ||x  -  z||  \mleq{}  ||x  -  y  +  y  -  z||


By

---

Latex:
(Assert  \mkleeneopen{}x  -  y  +  y  -  z  \mequiv{}  x  -  z\mkleeneclose{}\mcdot{}  THENM  (RWO    "-1"  0  THEN  Auto))

---

Home Index