---

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


1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. |x ⋅ y| < (||x|| * ||y||)
⊢ r0 < ||x - y||
BY
{ (((BLemma `square-rless-implies` THEN Auto) THEN (RWO "rnexp0" 0 THENA Auto))
   THEN (RWW "rv-norm-squared rv-ip-sub-squared" 0 THENA Auto)
   THEN (InstLemma `rnexp-rless` [⌜|x ⋅ y|⌝;⌜||x|| * ||y||⌝;⌜2⌝]⋅ 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||)
\mvdash{}  r0  <  ||x  -  y||


By

---

Latex:
(((BLemma  `square-rless-implies`  THEN  Auto)  THEN  (RWO  "rnexp0"  0  THENA  Auto))
  THEN  (RWW  "rv-norm-squared  rv-ip-sub-squared"  0  THENA  Auto)
  THEN  (InstLemma  `rnexp-rless`  [\mkleeneopen{}|x  \mcdot{}  y|\mkleeneclose{};\mkleeneopen{}||x||  *  ||y||\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index