---

Step * 1 1 of Lemma rv-Cauchy-Schwarz-equality'


1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. |a ⋅ b| = (||a|| * ||b||)
⊢ a ⋅ b^2 = |a ⋅ b^2|
BY
{ (RWO "rabs-of-nonneg" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point
3.  b  :  Point
4.  |a  \mcdot{}  b|  =  (||a||  *  ||b||)
\mvdash{}  a  \mcdot{}  b\^{}2  =  |a  \mcdot{}  b\^{}2|


By

---

Latex:
(RWO  "rabs-of-nonneg"  0  THEN  Auto)

---

Home Index