---

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


1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
3. ∃M:n:ℕ ⟶ (ℕn ⟶ (i:ℕ × ℕB[i])) ⟶ (ℤ?)
    ∀f:ℕ ⟶ (i:ℕ × ℕB[i])
      ((∃n:ℕ. ((M n f) = (inl ((λf.(F (λi.let j,n = f i in if (j =z i) then n else 0 fi ))) f)) ∈ (ℤ?)))
      ∧ (∀n:ℕ
           (M n f) = (inl ((λf.(F (λi.let j,n = f i in if (j =z i) then n else 0 fi ))) f)) ∈ (ℤ?) 
           supposing ↑isl(M n f)))
⊢ ∃M:n:ℕ ⟶ (i:ℕn ⟶ ℕB[i]) ⟶ (ℤ?) [(∀f:i:ℕ ⟶ ℕB[i]
                                        ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℤ?)))
                                        ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℤ?) supposing ↑isl(M n f))))]
BY
{ D -1 }

1
1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
3. M : n:ℕ ⟶ (ℕn ⟶ (i:ℕ × ℕB[i])) ⟶ (ℤ?)
4. ∀f:ℕ ⟶ (i:ℕ × ℕB[i])
     ((∃n:ℕ. ((M n f) = (inl ((λf.(F (λi.let j,n = f i in if (j =z i) then n else 0 fi ))) f)) ∈ (ℤ?)))
     ∧ (∀n:ℕ
          (M n f) = (inl ((λf.(F (λi.let j,n = f i in if (j =z i) then n else 0 fi ))) f)) ∈ (ℤ?) 
          supposing ↑isl(M n f)))
⊢ ∃M:n:ℕ ⟶ (i:ℕn ⟶ ℕB[i]) ⟶ (ℤ?) [(∀f:i:ℕ ⟶ ℕB[i]
                                        ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℤ?)))
                                        ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℤ?) supposing ↑isl(M n f))))]

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  F  :  (i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  \mBbbZ{}
3.  \mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i]))  {}\mrightarrow{}  (\mBbbZ{}?)
        \mforall{}f:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i])
            ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  ((\mlambda{}f.(F  (\mlambda{}i.let  j,n  =  f  i  in  if  (j  =\msubz{}  i)  then  n  else  0  fi  )))  f))))
            \mwedge{}  (\mforall{}n:\mBbbN{}
                      (M  n  f)  =  (inl  ((\mlambda{}f.(F  (\mlambda{}i.let  j,n  =  f  i  in  if  (j  =\msubz{}  i)  then  n  else  0  fi  )))  f)) 
                      supposing  \muparrow{}isl(M  n  f)))
\mvdash{}  \mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  (\mBbbZ{}?)  [(\mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i]
                                                                                ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  (F  f))))
                                                                                \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (inl  (F  f))  supposing  \muparrow{}isl(M  n  f))))]


By

---

Latex:
D  -1

---

Home Index