---

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


1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. f : i:ℕn ⟶ ℤ
6. N : ℕ+
7. (k * 8 * n) = N ∈ ℕ+
8. ∀i:ℕn. ((|(r(f i)/r(N))| ≤ |p i|) ∧ (|(p i) - (r(f i)/r(N))| ≤ (r(2)/r(k * 2 * n))))
9. d(p;λi.(r(f i))/N) ≤ (rsqrt(r(n)) * (r(2)/r(k * 2 * n)))
10. rsqrt(r(n)) ≤ r(n)
11. (r(2)/r(k * 2 * n)) = (r1/r(k) * r(n))
⊢ (rsqrt(r(n)) * (r1/r(k) * r(n))) ≤ (r1/r(k))
BY
{ ((GenConcl ⌜r(k) = x ∈ {x:ℝ| r0 < x} ⌝⋅ THENA Auto) THEN nRMul ⌜x⌝ 0⋅ THEN Auto) }

1
1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. f : i:ℕn ⟶ ℤ
6. N : ℕ+
7. (k * 8 * n) = N ∈ ℕ+
8. ∀i:ℕn. ((|(r(f i)/r(N))| ≤ |p i|) ∧ (|(p i) - (r(f i)/r(N))| ≤ (r(2)/r(k * 2 * n))))
9. d(p;λi.(r(f i))/N) ≤ (rsqrt(r(n)) * (r(2)/r(k * 2 * n)))
10. rsqrt(r(n)) ≤ r(n)
11. (r(2)/r(k * 2 * n)) = (r1/r(k) * r(n))
12. x : {x:ℝ| r0 < x} 
13. r(k) = x ∈ {x:ℝ| r0 < x} 
⊢ x * r(n) ≠ r0

2
1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. f : i:ℕn ⟶ ℤ
6. N : ℕ+
7. (k * 8 * n) = N ∈ ℕ+
8. ∀i:ℕn. ((|(r(f i)/r(N))| ≤ |p i|) ∧ (|(p i) - (r(f i)/r(N))| ≤ (r(2)/r(k * 2 * n))))
9. d(p;λi.(r(f i))/N) ≤ (rsqrt(r(n)) * (r(2)/r(k * 2 * n)))
10. rsqrt(r(n)) ≤ r(n)
11. (r(2)/r(k * 2 * n)) = (r1/r(k) * r(n))
12. x : {x:ℝ| r0 < x} 
13. r(k) = x ∈ {x:ℝ| r0 < x} 
⊢ (rsqrt(r(n))/r(n)) ≤ r1

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbR{}\^{}n
4.  ||p||  \mleq{}  r1
5.  f  :  i:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
6.  N  :  \mBbbN{}\msupplus{}
7.  (k  *  8  *  n)  =  N
8.  \mforall{}i:\mBbbN{}n.  ((|(r(f  i)/r(N))|  \mleq{}  |p  i|)  \mwedge{}  (|(p  i)  -  (r(f  i)/r(N))|  \mleq{}  (r(2)/r(k  *  2  *  n))))
9.  d(p;\mlambda{}i.(r(f  i))/N)  \mleq{}  (rsqrt(r(n))  *  (r(2)/r(k  *  2  *  n)))
10.  rsqrt(r(n))  \mleq{}  r(n)
11.  (r(2)/r(k  *  2  *  n))  =  (r1/r(k)  *  r(n))
\mvdash{}  (rsqrt(r(n))  *  (r1/r(k)  *  r(n)))  \mleq{}  (r1/r(k))


By

---

Latex:
((GenConcl  \mkleeneopen{}r(k)  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  nRMul  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index