---

Step * of Lemma strong-continuity3-half-squash

∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(strong-continuity3(T;F)) supposing (T ⊆r ℕ) ∧ (↓T)
BY
{ (InstLemma `strong-continuity2-half-squash` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (UnHalfSquash THENA Auto)
   THEN UnHalfSquashConcl
   THEN Auto) }

1
1. [T] : Type
2. T ⊆r ℕ
3. ↓T
4. F : (ℕ ⟶ T) ⟶ ℕ
5. strong-continuity2(T;F)
⊢ strong-continuity3(T;F)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `strong-continuity2-half-squash`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (UnHalfSquash  THENA  Auto)
  THEN  UnHalfSquashConcl
  THEN  Auto)

---

Home Index