---

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


1. B : ℕ ⟶ ℕ+
2. F : (i:ℕ ⟶ ℕB[i]) ⟶ ℤ
3. ∀F:(ℕ ⟶ (i:ℕ × ℕB[i])) ⟶ ℤ
     ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ (i:ℕ × ℕ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))))
⊢ ⇃(∃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 With ⌜λf.(F (λi.let j,n = f i in if (j =z i) then n else 0 fi ))⌝  THENA Auto)
   THEN (UnHalfSquash THENA Auto)
   THEN (UnHalfSquashConcl THENA Auto)) }

1
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))))]

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  F  :  (i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  \mBbbZ{}
3.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i]))  {}\mrightarrow{}  \mBbbZ{}
          \00D9(\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  (F  f))))  \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (inl  (F  f))  supposing  \muparrow{}isl(M  n  f))))
\mvdash{}  \00D9(\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  With  \mkleeneopen{}\mlambda{}f.(F  (\mlambda{}i.let  j,n  =  f  i  in  if  (j  =\msubz{}  i)  then  n  else  0  fi  ))\mkleeneclose{}    THENA  Auto)
  THEN  (UnHalfSquash  THENA  Auto)
  THEN  (UnHalfSquashConcl  THENA  Auto))

---

Home Index