---

Step * 1 1 of Lemma ip-triangle-implies-separated


1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. |x ⋅ y| < (||x|| * ||y||)
5. |x ⋅ y|^2 < ||x|| * ||y||^2
⊢ r0 < ((x^2 - r(2) * x ⋅ y) + y^2)
BY
{ (RWO "rv-norm-squared<" 0 THENA Auto) }

1
1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. |x ⋅ y| < (||x|| * ||y||)
5. |x ⋅ y|^2 < ||x|| * ||y||^2
⊢ r0 < ((||x||^2 - r(2) * x ⋅ y) + ||y||^2)

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  Point
3.  y  :  Point
4.  |x  \mcdot{}  y|  <  (||x||  *  ||y||)
5.  |x  \mcdot{}  y|\^{}2  <  ||x||  *  ||y||\^{}2
\mvdash{}  r0  <  ((x\^{}2  -  r(2)  *  x  \mcdot{}  y)  +  y\^{}2)


By

---

Latex:
(RWO  "rv-norm-squared<"  0  THENA  Auto)

---

Home Index