---

Step * 2 1 2 of Lemma real-unit-ball-totally-bounded1


1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. ∀i:ℕn. ∃z:ℤ. ((|(r(z)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(z)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
6. f : i:ℕn ⟶ ℤ
7. ∀i:ℕn. ((|(r(f i)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(f i)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
8. x : ℕn
9. |(r(f x)/r(k * 8 * n))| ≤ r1
10. |p x| ≤ r1
⊢ f x ∈ {-(k * 8 * n)..(k * 8 * n) + 1-}
BY
{ (MoveToConcl (-2)
   THEN (GenConcl ⌜(k * 8 * n) = N ∈ ℕ+⌝⋅ THENA Auto)
   THEN All Thin
   THEN (Assert r0 < r(N) BY
               Auto)
   THEN (Assert r0 < |r(N)| BY
               Auto)
   THEN (RWW "rabs-rdiv rabs-int" 0 THENA Auto)
   THEN ((Subst' |N| ~ N 0 THENM D 0) THENA Auto)) }

1
1. n : ℕ+
2. f : i:ℕn ⟶ ℤ
3. x : ℕn
4. N : ℕ+
5. r0 < r(N)
6. r0 < |r(N)|
7. (r(|f x|)/r(N)) ≤ r1
⊢ f x ∈ {-N..N + 1-}

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbR{}\^{}n
4.  ||p||  \mleq{}  r1
5.  \mforall{}i:\mBbbN{}n
          \mexists{}z:\mBbbZ{}.  ((|(r(z)/r(k  *  8  *  n))|  \mleq{}  |p  i|)  \mwedge{}  (|(p  i)  -  (r(z)/r(k  *  8  *  n))|  \mleq{}  (r(2)/r(k  *  2  *  n))))
6.  f  :  i:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
7.  \mforall{}i:\mBbbN{}n
          ((|(r(f  i)/r(k  *  8  *  n))|  \mleq{}  |p  i|)  \mwedge{}  (|(p  i)  -  (r(f  i)/r(k  *  8  *  n))|  \mleq{}  (r(2)/r(k  *  2  *  n))))
8.  x  :  \mBbbN{}n
9.  |(r(f  x)/r(k  *  8  *  n))|  \mleq{}  r1
10.  |p  x|  \mleq{}  r1
\mvdash{}  f  x  \mmember{}  \{-(k  *  8  *  n)..(k  *  8  *  n)  +  1\msupminus{}\}


By

---

Latex:
(MoveToConcl  (-2)
  THEN  (GenConcl  \mkleeneopen{}(k  *  8  *  n)  =  N\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  (Assert  r0  <  r(N)  BY
                          Auto)
  THEN  (Assert  r0  <  |r(N)|  BY
                          Auto)
  THEN  (RWW  "rabs-rdiv  rabs-int"  0  THENA  Auto)
  THEN  ((Subst'  |N|  \msim{}  N  0  THENM  D  0)  THENA  Auto))

---

Home Index