---

Step * of Lemma ip-weak-triangle-inequality

∀rv:InnerProductSpace. ∀a,b,x,p:Point.  (ax=ab ⇒ a_x_p ⇒ bp ≥ xp)
BY
{ (Auto
   THEN UnfoldTopAb (-2)
   THEN (FLemma `ip-dist-between` [-1] THENA Auto)
   THEN (Assert ||a - p|| ≤ (||a - b|| + ||b - p||) BY
               Auto)
   THEN (RWO "-2" (-1) THENA Auto)
   THEN (RWO "6" (-1) THENA Auto)
   THEN (nRAdd ⌜-(||a - b||)⌝ (-1)⋅ THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. x : Point
5. p : Point
6. ||a - x|| = ||a - b||
7. a_x_p
8. ||a - p|| = (||a - x|| + ||x - p||)
9. ||x - p|| ≤ ||b - p||
⊢ bp ≥ xp

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,x,p:Point.    (ax=ab  {}\mRightarrow{}  a\_x\_p  {}\mRightarrow{}  bp  \mgeq{}  xp)


By

---

Latex:
(Auto
  THEN  UnfoldTopAb  (-2)
  THEN  (FLemma  `ip-dist-between`  [-1]  THENA  Auto)
  THEN  (Assert  ||a  -  p||  \mleq{}  (||a  -  b||  +  ||b  -  p||)  BY
                          Auto)
  THEN  (RWO  "-2"  (-1)  THENA  Auto)
  THEN  (RWO  "6"  (-1)  THENA  Auto)
  THEN  (nRAdd  \mkleeneopen{}-(||a  -  b||)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))

---

Home Index