---

Step * of Lemma ip-line-circle

No Annotations
∀rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| a # b} . ∀p:{p:Point(rv)| ab ≥ ap} . ∀q:{q:Point(rv)| 
                                                                                             p # q ∧ aq ≥ ab} .
  ∃u:{u:Point(rv)| ab=au ∧ q_u_p} . (∃v:Point(rv) [(ab=av ∧ q_p_v)])
BY
{ (InstLemma `ip-line-circle-1` [] THEN RepeatFor 5 ((ParallelLast' THENA Auto)) THEN RepeatFor 3 ((D -1 THENA Auto))) }

1
.....antecedent..... 
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : {b:Point(rv)| a # b} 
4. p : {p:Point(rv)| ab ≥ ap} 
5. q : {q:Point(rv)| p # q ∧ aq ≥ ab} 
⊢ ||p - a|| ≤ ||a - b||

2
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : {b:Point(rv)| a # b} 
4. p : {p:Point(rv)| ab ≥ ap} 
5. q : {q:Point(rv)| p # q ∧ aq ≥ ab} 
6. (||a - b|| ≤ ||q - a||)
⇒ (∃u:{u:Point(rv)| ab=au ∧ q_u_p} 
     ∃v:{v:Point(rv)| ab=av ∧ q_p_v} . ((||a - p|| < ||a - b||) ⇒ (p # v ∧ ((||a - b|| < ||a - q||) ⇒ q # u))))
⊢ ∃u:{u:Point(rv)| ab=au ∧ q_u_p} . (∃v:Point(rv) [(ab=av ∧ q_p_v)])

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}a:Point(rv).  \mforall{}b:\{b:Point(rv)|  a  \#  b\}  .  \mforall{}p:\{p:Point(rv)|  ab  \mgeq{}  ap\}  .
\mforall{}q:\{q:Point(rv)|  p  \#  q  \mwedge{}  aq  \mgeq{}  ab\}  .
    \mexists{}u:\{u:Point(rv)|  ab=au  \mwedge{}  q\_u\_p\}  .  (\mexists{}v:Point(rv)  [(ab=av  \mwedge{}  q\_p\_v)])


By

---

Latex:
(InstLemma  `ip-line-circle-1`  []
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
  THEN  RepeatFor  3  ((D  -1  THENA  Auto)))

---

Home Index