---

Step * of Lemma unit-ball-approx-subtype

∀[k,n,m:ℕ].  unit-ball-approx(m;k) ⊆r unit-ball-approx(n;k) supposing n ≤ m
BY
{ (Intros THEN (D 0 THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. k : ℕ
2. n : ℕ
3. m : ℕ
4. n ≤ m
5. x : ℕm ⟶ {-k..k + 1-}
6. Σ((x i) * (x i) | i < m) ≤ (k * k)
⊢ Σ((x i) * (x i) | i < n) ≤ (k * k)

---

Latex:

---

Latex:
\mforall{}[k,n,m:\mBbbN{}].    unit-ball-approx(m;k)  \msubseteq{}r  unit-ball-approx(n;k)  supposing  n  \mleq{}  m


By

---

Latex:
(Intros  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  MemTypeCD  THEN  Auto)

---

Home Index