---

Step * of Lemma rv-midpoint-unique

No Annotations
∀rv:InnerProductSpace. ∀a,b,m:Point(rv).
  ((||m - a|| = (||b - a||/r(2))) ∧ (||m - b|| = (||b - a||/r(2))) ⇐⇒ m ≡ (r1/r(2))*a + b)
BY
{ Auto }

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

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

3
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))

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,m:Point(rv).
    ((||m  -  a||  =  (||b  -  a||/r(2)))  \mwedge{}  (||m  -  b||  =  (||b  -  a||/r(2)))  \mLeftarrow{}{}\mRightarrow{}  m  \mequiv{}  (r1/r(2))*a  +  b)


By

---

Latex:
Auto

---

Home Index