---

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


1. v : ℕ+
2. K : ℕv ⟶ ℕ
3. t : ℕv
⊢ (∃b∈map(K;upto(v)). (K t) ≤ b)
BY
{ (D 0 With ⌜t⌝  THEN Auto) }

1
1. v : ℕ+
2. K : ℕv ⟶ ℕ
3. t : ℕv
⊢ (K t) ≤ map(K;upto(v))[t]

---

Latex:

---

Latex:

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


By

---

Latex:
(D  0  With  \mkleeneopen{}t\mkleeneclose{}    THEN  Auto)

---

Home Index