---

Step * 1 1 of Lemma unit-ball-approxn

.....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)
BY
{ ((Assert 0 < n BY Auto) THEN ((RWO "sum-unroll" (-2) THENM Reduce -2) THENA Auto)) }

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

---

Latex:

---

Latex:
.....wf..... 
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{}  x  \mmember{}  unit-ball-approx(n  -  1;k)


By

---

Latex:
((Assert  0  <  n  BY  Auto)  THEN  ((RWO  "sum-unroll"  (-2)  THENM  Reduce  -2)  THENA  Auto))

---

Home Index