---

Step * 2 1 1 1 1 of Lemma general-cantor-to-int-uniform-continuity-half-squashed


1. v : ℕ+
2. K : ℕv ⟶ ℕ
3. t : ℕv
⊢ (K t) ≤ map(K;upto(v))[t]
BY
{ ((RWO "select-map" 0 THENA Auto) THEN RWO "select-upto" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  v  :  \mBbbN{}\msupplus{}
2.  K  :  \mBbbN{}v  {}\mrightarrow{}  \mBbbN{}
3.  t  :  \mBbbN{}v
\mvdash{}  (K  t)  \mleq{}  map(K;upto(v))[t]


By

---

Latex:
((RWO  "select-map"  0  THENA  Auto)  THEN  RWO  "select-upto"  0  THEN  Auto)

---

Home Index