---

Step * of Lemma ip-extend-lemma

No Annotations
∀rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| a # b} . ∀dcd:{d:ℝ| r0 ≤ d} .
  (∃x:Point(rv) [(a_b_x ∧ (||b - x|| = dcd))])
BY
{ (Auto THEN (Assert r0 < ||a - b|| BY EAuto 1) THEN (Assert r0 ≤ dcd BY Auto)) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : {b:Point(rv)| a # b} 
4. dcd : {d:ℝ| r0 ≤ d} 
5. r0 < ||a - b||
6. r0 ≤ dcd
⊢ ∃x:Point(rv) [(a_b_x ∧ (||b - x|| = dcd))]

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}a:Point(rv).  \mforall{}b:\{b:Point(rv)|  a  \#  b\}  .  \mforall{}dcd:\{d:\mBbbR{}|  r0  \mleq{}  d\}  .
    (\mexists{}x:Point(rv)  [(a\_b\_x  \mwedge{}  (||b  -  x||  =  dcd))])


By

---

Latex:
(Auto  THEN  (Assert  r0  <  ||a  -  b||  BY  EAuto  1)  THEN  (Assert  r0  \mleq{}  dcd  BY  Auto))

---

Home Index