---

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


1. B : ℕ ⟶ ℕ+
2. F : (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
3. n : ℕ
4. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))
5. j : ℕ
6. j < n
⊢ Dec(∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
BY
{ ((Assert finite(i:ℕn ⟶ ℕB[i]) BY
          (BLemma `finite-function` THEN Auto))
   THEN (Assert ∀p,q:i:ℕn ⟶ ℕB[i].  Dec(∀i:ℕj. ((p i) = (q i) ∈ ℕB[i])) BY
               Auto)
   THEN (Assert ∀p,q:i:ℕn ⟶ ℕB[i].  Dec(p = q ∈ (i:ℕj ⟶ ℕB[i])) BY
               (RepeatFor 4 (ParallelLast) THEN ((ParallelLast THEN Auto) ORELSE (FunExt THEN Auto))))) }

1
1. B : ℕ ⟶ ℕ+
2. F : (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
3. n : ℕ
4. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))
5. j : ℕ
6. j < n
7. finite(i:ℕn ⟶ ℕB[i])
8. ∀p,q:i:ℕn ⟶ ℕB[i].  Dec(∀i:ℕj. ((p i) = (q i) ∈ ℕB[i]))
9. ∀p,q:i:ℕn ⟶ ℕB[i].  Dec(p = q ∈ (i:ℕj ⟶ ℕB[i]))
⊢ Dec(∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  F  :  (k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[k])  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}
4.  \mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))
5.  j  :  \mBbbN{}
6.  j  <  n
\mvdash{}  Dec(\mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))


By

---

Latex:
((Assert  finite(i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i])  BY
                (BLemma  `finite-function`  THEN  Auto))
  THEN  (Assert  \mforall{}p,q:i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i].    Dec(\mforall{}i:\mBbbN{}j.  ((p  i)  =  (q  i)))  BY
                          Auto)
  THEN  (Assert  \mforall{}p,q:i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i].    Dec(p  =  q)  BY
                          (RepeatFor  4  (ParallelLast)
                            THEN  ((ParallelLast  THEN  Auto)  ORELSE  (FunExt  THEN  Auto))
                            )))

---

Home Index