---

Step * of Lemma strong-continuity2_biject

∀[T,S:Type].
  ∀g:S ⟶ ℕ
    (Bij(S;ℕ;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
{ (InstLemma `strong-continuity2_biject_retract` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D -1 With ⌜ℕ⌝  THENA Auto)
   THEN (InstHyp  [⌜λx.x⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T,S:Type].
    \mforall{}g:S  {}\mrightarrow{}  \mBbbN{}
        (Bij(S;\mBbbN{};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:
(InstLemma  `strong-continuity2\_biject\_retract`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  -1  With  \mkleeneopen{}\mBbbN{}\mkleeneclose{}    THENA  Auto)
  THEN  (InstHyp    [\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2)
  THEN  Trivial)

---

Home Index