---

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


1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
⊢ ||x + y||^2 ≤ ||x|| + ||y||^2
BY
{ ((RWO "rv-norm-squared" 0 THENA Auto) THEN (RWO "rnexp2" 0 THENA Auto) THEN (nRNorm 0 THENA Auto)) }

1
1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
⊢ x + y^2 ≤ ((||x|| * ||x||) + (r(2) * ||x|| * ||y||) + (||y|| * ||y||))

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  Point(rv)
3.  y  :  Point(rv)
\mvdash{}  ||x  +  y||\^{}2  \mleq{}  ||x||  +  ||y||\^{}2


By

---

Latex:
((RWO  "rv-norm-squared"  0  THENA  Auto)  THEN  (RWO  "rnexp2"  0  THENA  Auto)  THEN  (nRNorm  0  THENA  Auto))

---

Home Index