---

Step * of Lemma length-rneq-real-vec-sep

∀n:ℕ. ∀x,v:ℝ^n.  (||v|| ≠ ||x|| ⇒ x ≠ v)
BY
{ (Auto
   THEN (RWO "rneq-iff-rabs" (-1) THENA Auto)
   THEN (Assert |||v|| - ||x||| ≤ d(x;v) BY
               Auto)
   THEN UnfoldTopAb 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,v:\mBbbR{}\^{}n.    (||v||  \mneq{}  ||x||  {}\mRightarrow{}  x  \mneq{}  v)


By

---

Latex:
(Auto
  THEN  (RWO  "rneq-iff-rabs"  (-1)  THENA  Auto)
  THEN  (Assert  |||v||  -  ||x|||  \mleq{}  d(x;v)  BY
                          Auto)
  THEN  UnfoldTopAb  0
  THEN  Auto)

---

Home Index