---

Step * 1 1 1 of Lemma unit-ball-approxn


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)
BY
{ (Assert 0 ≤ ((x (n - 1)) * (x (n - 1))) BY
         ((GenConcl ⌜(x (n - 1)) = z ∈ ℤ⌝⋅ THENA Auto) THEN All Thin THEN 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
6. 0 ≤ ((x (n - 1)) * (x (n - 1)))
⊢ x ∈ unit-ball-approx(n - 1;k)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  x  :  \mBbbN{}n  {}\mrightarrow{}  \{-k..k  +  1\msupminus{}\}
4.  (\mSigma{}((x  i)  *  (x  i)  |  i  <  n  -  1)  +  ((x  (n  -  1))  *  (x  (n  -  1))))  \mleq{}  (k  *  k)
5.  0  <  n
\mvdash{}  x  \mmember{}  unit-ball-approx(n  -  1;k)


By

---

Latex:
(Assert  0  \mleq{}  ((x  (n  -  1))  *  (x  (n  -  1)))  BY
              ((GenConcl  \mkleeneopen{}(x  (n  -  1))  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin  THEN  Auto))

---

Home Index