---

Step * 1 of Lemma ip-line-circle-1

.....assertion..... 
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. p : Point(rv)
5. q : Point(rv)
6. a # b
7. p # q
8. ||p - a|| ≤ ||a - b||
9. ||a - b|| ≤ ||q - a||
⊢ p - a # q - a
BY
{ EAuto 1 }

---

Latex:

---

Latex:
.....assertion..... 
1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  Point(rv)
4.  p  :  Point(rv)
5.  q  :  Point(rv)
6.  a  \#  b
7.  p  \#  q
8.  ||p  -  a||  \mleq{}  ||a  -  b||
9.  ||a  -  b||  \mleq{}  ||q  -  a||
\mvdash{}  p  -  a  \#  q  -  a


By

---

Latex:
EAuto  1

---

Home Index