---

Step * 3 of Lemma rv-midpoint-unique


1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. m : Point(rv)
5. m ≡ (r1/r(2))*a + b
⊢ ||m - b|| = (||b - a||/r(2))
BY
{ (RW (AddrC [2;1] (LemmaC `rv-norm-sub`)) 0 THENA Auto) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. m : Point(rv)
5. m ≡ (r1/r(2))*a + b
⊢ ||m - b|| = (||a - b||/r(2))

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  Point(rv)
4.  m  :  Point(rv)
5.  m  \mequiv{}  (r1/r(2))*a  +  b
\mvdash{}  ||m  -  b||  =  (||b  -  a||/r(2))


By

---

Latex:
(RW  (AddrC  [2;1]  (LemmaC  `rv-norm-sub`))  0  THENA  Auto)

---

Home Index