---

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


1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
⊢ ⇃(∀i:ℕ. ∀K:ℕB[i] ⟶ ℕ.  (∃Bnd:ℕ [(∀t:ℕB[i]. ((K t) ≤ Bnd))]))
BY
{ ((UnHalfSquashConcl THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (GenConclTerm ⌜B[i]⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. v : ℕ+
2. K : ℕv ⟶ ℕ
⊢ ∃Bnd:ℕ [(∀t:ℕv. ((K t) ≤ Bnd))]

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  F  :  (i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  \00D9(\mforall{}i:\mBbbN{}.  \mforall{}K:\mBbbN{}B[i]  {}\mrightarrow{}  \mBbbN{}.    (\mexists{}Bnd:\mBbbN{}  [(\mforall{}t:\mBbbN{}B[i].  ((K  t)  \mleq{}  Bnd))]))


By

---

Latex:
((UnHalfSquashConcl  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}B[i]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index