---

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


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-}
BY
{ (nRMul ⌜r(N)⌝ (-1)⋅
   THEN (RWO  "rleq-int" (-1) THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜f x⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. N : ℕ+
2. v : ℤ
⊢ (|v| ≤ N) ⇒ (v ∈ {-N..N + 1-})

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  f  :  i:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
3.  x  :  \mBbbN{}n
4.  N  :  \mBbbN{}\msupplus{}
5.  r0  <  r(N)
6.  r0  <  |r(N)|
7.  (r(|f  x|)/r(N))  \mleq{}  r1
\mvdash{}  f  x  \mmember{}  \{-N..N  +  1\msupminus{}\}


By

---

Latex:
(nRMul  \mkleeneopen{}r(N)\mkleeneclose{}  (-1)\mcdot{}
  THEN  (RWO    "rleq-int"  (-1)  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}f  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index