---

Step * of Lemma rv-weak-triangle-inequality2

∀n:ℕ. ∀a,b,x,p:ℝ^n.  (ax=ab ⇒ a_x_p ⇒ bp ≥ xp)
BY
{ ((Auto THEN UnfoldTopAb (-2))
   THEN (FLemma `rv-be-dist` [-1] THENA Auto)
   THEN (InstLemma `real-vec-triangle-inequality` [⌜n⌝;⌜a⌝;⌜b⌝;⌜p⌝]⋅ THENA Auto)
   THEN (RWO "-2" (-1) THENA Auto)
   THEN (RWO "6" (-1) THENA Auto)
   THEN (nRAdd ⌜-(d(a;b))⌝ (-1)⋅ THENA Auto)) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. x : ℝ^n
5. p : ℝ^n
6. d(a;x) = d(a;b)
7. a_x_p
8. d(a;p) = (d(a;x) + d(x;p))
9. d(x;p) ≤ d(b;p)
⊢ bp ≥ xp

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,x,p:\mBbbR{}\^{}n.    (ax=ab  {}\mRightarrow{}  a\_x\_p  {}\mRightarrow{}  bp  \mgeq{}  xp)


By

---

Latex:
((Auto  THEN  UnfoldTopAb  (-2))
  THEN  (FLemma  `rv-be-dist`  [-1]  THENA  Auto)
  THEN  (InstLemma  `real-vec-triangle-inequality`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-2"  (-1)  THENA  Auto)
  THEN  (RWO  "6"  (-1)  THENA  Auto)
  THEN  (nRAdd  \mkleeneopen{}-(d(a;b))\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))

---

Home Index