---

Step * of Lemma real-vec-sep-0-iff

No Annotations
∀n:ℕ. ∀x:ℝ^n.  (x ≠ λi.r0 ⇐⇒ r0 < x⋅x)
BY
{ (RepUR ``real-vec-sep real-vec-dist`` 0
   THEN Auto
   THEN (Assert req-vec(n;x - λi.r0;x) BY
               (D 0 THEN RepUR ``real-vec-sub`` 0 THEN Auto))) }

1
1. n : ℕ
2. x : ℝ^n
3. r0 < ||x - λi.r0||
4. req-vec(n;x - λi.r0;x)
⊢ r0 < x⋅x

2
1. n : ℕ
2. x : ℝ^n
3. r0 < x⋅x
4. req-vec(n;x - λi.r0;x)
⊢ r0 < ||x - λi.r0||

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}x:\mBbbR{}\^{}n.    (x  \mneq{}  \mlambda{}i.r0  \mLeftarrow{}{}\mRightarrow{}  r0  <  x\mcdot{}x)


By

---

Latex:
(RepUR  ``real-vec-sep  real-vec-dist``  0
  THEN  Auto
  THEN  (Assert  req-vec(n;x  -  \mlambda{}i.r0;x)  BY
                          (D  0  THEN  RepUR  ``real-vec-sub``  0  THEN  Auto)))

---

Home Index