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


1. : ℕ ⟶ ℕ+
2. (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
3. : ℕ
4. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f g ∈ (i:ℕn ⟶ ℕB[i]))  ((F f) (F g) ∈ ℤ))
5. : ℕ
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]))
10. Dec(∃p,q:i:ℕn ⟶ ℕB[i]
         ((p q ∈ (i:ℕj ⟶ ℕB[i]))
         ∧ ((F i.if i <then else fi )) (F i.if i <then else fi )) ∈ ℤ))))
⊢ Dec(∀f,g:i:ℕ ⟶ ℕB[i].  ((f g ∈ (i:ℕj ⟶ ℕB[i]))  ((F f) (F g) ∈ ℤ)))
BY
-1 }

1
1. : ℕ ⟶ ℕ+
2. (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
3. : ℕ
4. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f g ∈ (i:ℕn ⟶ ℕB[i]))  ((F f) (F g) ∈ ℤ))
5. : ℕ
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]))
10. ∃p,q:i:ℕn ⟶ ℕB[i]
     ((p q ∈ (i:ℕj ⟶ ℕB[i]))
     ∧ ((F i.if i <then else fi )) (F i.if i <then else fi )) ∈ ℤ)))
⊢ Dec(∀f,g:i:ℕ ⟶ ℕB[i].  ((f g ∈ (i:ℕj ⟶ ℕB[i]))  ((F f) (F g) ∈ ℤ)))

2
1. : ℕ ⟶ ℕ+
2. (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
3. : ℕ
4. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f g ∈ (i:ℕn ⟶ ℕB[i]))  ((F f) (F g) ∈ ℤ))
5. : ℕ
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]))
10. ¬(∃p,q:i:ℕn ⟶ ℕB[i]
       ((p q ∈ (i:ℕj ⟶ ℕB[i]))
       ∧ ((F i.if i <then else fi )) (F i.if i <then else fi )) ∈ ℤ))))
⊢ 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
7.  finite(i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i])
8.  \mforall{}p,q:i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i].    Dec(\mforall{}i:\mBbbN{}j.  ((p  i)  =  (q  i)))
9.  \mforall{}p,q:i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i].    Dec(p  =  q)
10.  Dec(\mexists{}p,q:i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i]
                  ((p  =  q)
                  \mwedge{}  (\mneg{}((F  (\mlambda{}i.if  i  <z  n  then  p  i  else  0  fi  ))  =  (F  (\mlambda{}i.if  i  <z  n  then  q  i  else  0  fi  ))))))
\mvdash{}  Dec(\mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))


By


Latex:
D  -1




Home Index