---

Step * of Lemma uniform-continuity-pi2-dec-ext

∀T:Type. ∀F:(ℕ ⟶ 𝔹) ⟶ T. ∀n:ℕ.  ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ Dec(ucB(T;F;n)))
BY
{ Extract of Obid: uniform-continuity-pi2-dec
  not unfolding  ext2Cantor extl2Cantor listops upto simple-finite-cantor-decider
  finishing with Auto
  normalizes to:
  
  λT,F,n,g. case FiniteCantorDecide(λs.if g (F ext2Cantor(n;s;inl Ax)) (F ext2Cantor(n;s;inr Ax ))
                                       then inr (λ_.Ax) 
                                       else inl (λ_.Ax)
                                       fi ;n;λx.x)
            of inl(p) =>
            let s,f = p 
            in inr (λ_.(f Ax)) 
            | inr(_) =>
            inl (λs.Ax) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.  \mforall{}n:\mBbbN{}.    ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  Dec(ucB(T;F;n)))


By

---

Latex:
Extract  of  Obid:  uniform-continuity-pi2-dec
not  unfolding    ext2Cantor  extl2Cantor  listops  upto  simple-finite-cantor-decider
finishing  with  Auto
normalizes  to:

\mlambda{}T,F,n,g.  case  FiniteCantorDecide(\mlambda{}s.if  g  (F  ext2Cantor(n;s;inl  Ax))  (F  ext2Cantor(n;s;inr  Ax  ))
                                                                          then  inr  (\mlambda{}$_{}$.Ax) 
                                                                          else  inl  (\mlambda{}$_{}$.Ax)
                                                                          fi  ;n;\mlambda{}x.x)
                    of  inl(p)  =>
                    let  s,f  =  p 
                    in  inr  (\mlambda{}$_{}$.(f  Ax)) 
                    |  inr($_{}$)  =>
                    inl  (\mlambda{}s.Ax)

---

Home Index