---

Step * of Lemma infinity-norm-rneq-real-vec-sep

No Annotations
∀n:ℕ+. ∀x,v:ℝ^n.  (||v||∞ ≠ ||x||∞ ⇒ x ≠ v)
BY
{ ((RWO "real-vec-sep-iff" 0 THENA Auto)
   THEN InductionOnNat
   THEN Auto
   THEN (RWO "real-vec-infinity-norm-req" (-1) THENA Auto)
   THEN Reduce -1
   THEN (OReduce (-1) THENA Auto)) }

1
1. n : ℕ+
2. x : ℝ^1
3. v : ℝ^1
4. |v 0| ≠ |x 0|
⊢ ∃i:ℕ1. (r0 < |(x i) - v i|)

2
1. n : ℤ
2. 0 < n
3. ∀x,v:ℝ^n.  (||v||∞ ≠ ||x||∞ ⇒ (∃i:ℕn. (r0 < |(x i) - v i|)))
4. x : ℝ^n + 1
5. v : ℝ^n + 1
6. rmax(||v||∞;|v ((n + 1) - 1)|) ≠ rmax(||x||∞;|x ((n + 1) - 1)|)
⊢ ∃i:ℕn + 1. (r0 < |(x i) - v i|)

---

Latex:

---

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


By

---

Latex:
((RWO  "real-vec-sep-iff"  0  THENA  Auto)
  THEN  InductionOnNat
  THEN  Auto
  THEN  (RWO  "real-vec-infinity-norm-req"  (-1)  THENA  Auto)
  THEN  Reduce  -1
  THEN  (OReduce  (-1)  THENA  Auto))

---

Home Index