---

Step * of Lemma strong-continuity2-half-squash

∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(strong-continuity2(T;F)) supposing (T ⊆r ℕ) ∧ (↓T)
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⇃(basic-strong-continuity(T;F)) BY
               (UseWitness ⌜Kleene-M(F)⌝⋅ THEN Auto))
   THEN (UnHalfSquash THENA Auto)
   THEN (UnHalfSquashConcl THENA Auto)
   THEN InstLemma `basic-implies-strong-continuity2-ext` [⌜T⌝;⌜F⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}.  \00D9(strong-continuity2(T;F))  supposing  (T  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mdownarrow{}T)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \00D9(basic-strong-continuity(T;F))  BY
                          (UseWitness  \mkleeneopen{}Kleene-M(F)\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (UnHalfSquash  THENA  Auto)
  THEN  (UnHalfSquashConcl  THENA  Auto)
  THEN  InstLemma  `basic-implies-strong-continuity2-ext`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index