---

Step * of Lemma strong-continuity2_biject_retract-ext

∀[T,S,U:Type].
  ∀r:ℕ ⟶ U
    ((U ⊆r ℕ)
    ⇒ (∀x:U. ((r x) = x ∈ U))
    ⇒ (∀g:S ⟶ U
          (Bij(S;U;g)
          ⇒ (∀F:(ℕ ⟶ T) ⟶ S
                (strong-continuity2(T;g o F)
                ⇒ (∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
                     ∀f:ℕ ⟶ T
                       ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?)))
                       ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f)))))))))
BY
{ Extract of Obid: strong-continuity2_biject_retract
  normalizes to:
  
  λr,_,_,g,bi,F,sc2. let M,ea = sc2 
                     in <λn,f. case M n f of inl(m) => inl let x,y = bi in fst((y (r m))) | inr(x) => inr x 
                        , λf.<<let x,y = ea f in fst(x), Ax>, λn.Ax>
                        >
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}[T,S,U:Type].
    \mforall{}r:\mBbbN{}  {}\mrightarrow{}  U
        ((U  \msubseteq{}r  \mBbbN{})
        {}\mRightarrow{}  (\mforall{}x:U.  ((r  x)  =  x))
        {}\mRightarrow{}  (\mforall{}g:S  {}\mrightarrow{}  U
                    (Bij(S;U;g)
                    {}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  S
                                (strong-continuity2(T;g  o  F)
                                {}\mRightarrow{}  (\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (S?)
                                          \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T
                                              ((\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:
Extract  of  Obid:  strong-continuity2\_biject\_retract
normalizes  to:

\mlambda{}r,$_{}$,$_{}$,g,bi,F,sc2.  let  M,ea  =  sc2 
                                  in  <\mlambda{}n,f.  case  M  n  f
                                                      of  inl(m)  =>
                                                      inl  let  x,y  =  bi 
                                                              in  fst((y  (r  m)))
                                                      |  inr(x)  =>
                                                      inr  x 
                                        ,  \mlambda{}f.<<let  x,y  =  ea  f  in  fst(x),  Ax>,  \mlambda{}n.Ax>
                                        >
finishing  with  Auto

---

Home Index