---

Step * 2 1 of Lemma rv-gt-dist


1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. q : ℝ^n
5. d(a;q) < d(a;b)
6. w : ℝ^n
7. a_w_b
8. aw=aq
9. a_w_b
10. aw=aq
⊢ w ≠ b
BY
{ ((FLemma  `rv-be-dist` [-2] THENA Auto)
   THEN All (Unfold `rv-congruent`)
   THEN (RWO "-2" (-1) THENA Auto)
   THEN Unfold `real-vec-sep` 0
   THEN nRAdd ⌜-(d(a;q))⌝ (-1)⋅
   THEN RWO "-1<" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  q  :  \mBbbR{}\^{}n
5.  d(a;q)  <  d(a;b)
6.  w  :  \mBbbR{}\^{}n
7.  a\_w\_b
8.  aw=aq
9.  a\_w\_b
10.  aw=aq
\mvdash{}  w  \mneq{}  b


By

---

Latex:
((FLemma    `rv-be-dist`  [-2]  THENA  Auto)
  THEN  All  (Unfold  `rv-congruent`)
  THEN  (RWO  "-2"  (-1)  THENA  Auto)
  THEN  Unfold  `real-vec-sep`  0
  THEN  nRAdd  \mkleeneopen{}-(d(a;q))\mkleeneclose{}  (-1)\mcdot{}
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index