---

Step * of Lemma unit-ball-approxn

∀[k:ℕ]. ∀[n:ℕ+].
  unit-ball-approx(n;k) ≡ {f:ℕn ⟶ {-k..k + 1-}| 
                           ∃q:unit-ball-approx(n - 1;k)
                            ∃z:{-k..k + 1-}
                             (((Σ((q i) * (q i) | i < n - 1) + (z * z)) ≤ (k * k))
                             ∧ (∀i:ℕn - 1. ((f i) = (q i) ∈ ℤ))
                             ∧ ((f (n - 1)) = z ∈ ℤ))} 
BY
{ (Auto THEN RepeatFor 2 (D 0) THEN Auto THEN (D -1 THEN ExRepD) THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. k : ℕ
2. n : ℕ+
3. x : ℕn ⟶ {-k..k + 1-}
4. Σ((x i) * (x i) | i < n) ≤ (k * k)
⊢ ∃q:unit-ball-approx(n - 1;k)
   ∃z:{-k..k + 1-}
    (((Σ((q i) * (q i) | i < n - 1) + (z * z)) ≤ (k * k)) ∧ (∀i:ℕn - 1. ((x i) = (q i) ∈ ℤ)) ∧ ((x (n - 1)) = z ∈ ℤ))

2
.....set predicate..... 
1. k : ℕ
2. n : ℕ+
3. x : ℕn ⟶ {-k..k + 1-}
4. q : unit-ball-approx(n - 1;k)
5. z : {-k..k + 1-}
6. (Σ((q i) * (q i) | i < n - 1) + (z * z)) ≤ (k * k)
7. ∀i:ℕn - 1. ((x i) = (q i) ∈ ℤ)
8. (x (n - 1)) = z ∈ ℤ
⊢ Σ((x i) * (x i) | i < n) ≤ (k * k)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].
    unit-ball-approx(n;k)  \mequiv{}  \{f:\mBbbN{}n  {}\mrightarrow{}  \{-k..k  +  1\msupminus{}\}| 
                                                      \mexists{}q:unit-ball-approx(n  -  1;k)
                                                        \mexists{}z:\{-k..k  +  1\msupminus{}\}
                                                          (((\mSigma{}((q  i)  *  (q  i)  |  i  <  n  -  1)  +  (z  *  z))  \mleq{}  (k  *  k))
                                                          \mwedge{}  (\mforall{}i:\mBbbN{}n  -  1.  ((f  i)  =  (q  i)))
                                                          \mwedge{}  ((f  (n  -  1))  =  z))\} 


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  0)  THEN  Auto  THEN  (D  -1  THEN  ExRepD)  THEN  MemTypeCD  THEN  Auto)

---

Home Index