---

Step * 1 of Lemma unit-ball-approxn

.....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 ∈ ℤ))
BY
{ (InstConcl [⌜x⌝;⌜x (n - 1)⌝]⋅ THEN Auto) }

1
.....wf..... 
1. k : ℕ
2. n : ℕ+
3. x : ℕn ⟶ {-k..k + 1-}
4. Σ((x i) * (x i) | i < n) ≤ (k * k)
⊢ x ∈ unit-ball-approx(n - 1;k)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  x  :  \mBbbN{}n  {}\mrightarrow{}  \{-k..k  +  1\msupminus{}\}
4.  \mSigma{}((x  i)  *  (x  i)  |  i  <  n)  \mleq{}  (k  *  k)
\mvdash{}  \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.  ((x  i)  =  (q  i)))
        \mwedge{}  ((x  (n  -  1))  =  z))


By

---

Latex:
(InstConcl  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x  (n  -  1)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index