---

Step * of Lemma strong-continuity3-half-squash-equipollent

∀[T:Type]. ∀[B:Type]. (T ~ B ⇒ (∀F:(ℕ ⟶ B) ⟶ ℕ. ⇃(strong-continuity3(B;F)))) supposing (T ⊆r ℕ) ∧ (↓T)
BY
{ (Auto
   THEN RenameVar `e' (-2)
   THEN (Assert ⇃(strong-continuity3(T;λf.(F ((fst(e)) o f)))) BY
               (BLemma `strong-continuity3-half-squash` THEN Auto))
   THEN (UnHalfSquash THENA Auto)
   THEN UnHalfSquashConcl
   THEN Auto) }

1
1. [T] : Type
2. T ⊆r ℕ
3. ↓T
4. [B] : Type
5. e : T ~ B
6. F : (ℕ ⟶ B) ⟶ ℕ
7. strong-continuity3(T;λf.(F ((fst(e)) o f)))
⊢ strong-continuity3(B;F)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RenameVar  `e'  (-2)
  THEN  (Assert  \00D9(strong-continuity3(T;\mlambda{}f.(F  ((fst(e))  o  f))))  BY
                          (BLemma  `strong-continuity3-half-squash`  THEN  Auto))
  THEN  (UnHalfSquash  THENA  Auto)
  THEN  UnHalfSquashConcl
  THEN  Auto)

---

Home Index