---

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


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|)
BY
{ ((FLemma `rmax-rneq` [-1] THENM D -1) THENA Auto) }

1
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)|)
7. ||v||∞ ≠ ||x||∞
⊢ ∃i:ℕn + 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)|)
7. |v ((n + 1) - 1)| ≠ |x ((n + 1) - 1)|
⊢ ∃i:ℕn + 1. (r0 < |(x i) - v i|)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}x,v:\mBbbR{}\^{}n.    (||v||\minfty{}  \mneq{}  ||x||\minfty{}  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}n.  (r0  <  |(x  i)  -  v  i|)))
4.  x  :  \mBbbR{}\^{}n  +  1
5.  v  :  \mBbbR{}\^{}n  +  1
6.  rmax(||v||\minfty{};|v  ((n  +  1)  -  1)|)  \mneq{}  rmax(||x||\minfty{};|x  ((n  +  1)  -  1)|)
\mvdash{}  \mexists{}i:\mBbbN{}n  +  1.  (r0  <  |(x  i)  -  v  i|)


By

---

Latex:
((FLemma  `rmax-rneq`  [-1]  THENM  D  -1)  THENA  Auto)

---

Home Index